funfvop - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem funfvop 3788

Description: Ordered pair with function value. Part of Theorem 4.3(i) of [Monk1] p. 41.

**Assertion**
Ref	Expression
funfvop	⊢ ((Fun F ⋀ A ∈ dom F) → ⟨A, (F ‘A)⟩ ∈ F)

**Proof of Theorem funfvop**
Step	Hyp	Ref	Expression
1		fvex 3717	. . 3 ⊢ (F ‘A) ∈ V
2	1	isseti 1806	. 2 ⊢ ∃x x = (F ‘A)
3		visset 1804	. . . . . . 7 ⊢ x ∈ V
4	3	funopfvb 3741	. . . . . 6 ⊢ ((Fun F ⋀ A ∈ dom F) → ((F ‘A) = x ↔ ⟨A, x⟩ ∈ F))
5		opeq2 2479	. . . . . . . 8 ⊢ ((F ‘A) = x → ⟨A, (F ‘A)⟩ = ⟨A, x⟩)
6	5	eleq1d 1532	. . . . . . 7 ⊢ ((F ‘A) = x → (⟨A, (F ‘A)⟩ ∈ F ↔ ⟨A, x⟩ ∈ F))
7	6	biimprcd 156	. . . . . 6 ⊢ (⟨A, x⟩ ∈ F → ((F ‘A) = x → ⟨A, (F ‘A)⟩ ∈ F))
8	4, 7	syl6bi 214	. . . . 5 ⊢ ((Fun F ⋀ A ∈ dom F) → ((F ‘A) = x → ((F ‘A) = x → ⟨A, (F ‘A)⟩ ∈ F)))
9	8	pm2.43d 65	. . . 4 ⊢ ((Fun F ⋀ A ∈ dom F) → ((F ‘A) = x → ⟨A, (F ‘A)⟩ ∈ F))
10		eqcom 1469	. . . 4 ⊢ (x = (F ‘A) ↔ (F ‘A) = x)
11	9, 10	syl5ib 206	. . 3 ⊢ ((Fun F ⋀ A ∈ dom F) → (x = (F ‘A) → ⟨A, (F ‘A)⟩ ∈ F))
12	11	19.23adv 1209	. 2 ⊢ ((Fun F ⋀ A ∈ dom F) → (∃x x = (F ‘A) → ⟨A, (F ‘A)⟩ ∈ F))
13	2, 12	mpi 44	1 ⊢ ((Fun F ⋀ A ∈ dom F) → ⟨A, (F ‘A)⟩ ∈ F)

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 = wceq 953 ∈ wcel 955 ∃wex 977 ⟨cop 2401 dom cdm 3160 Fun wfun 3166 ‘cfv 3172

This theorem is referenced by: fvimacnv 3790 fnopfv 3796 fvelrn 3797 dff2 3802 funfvima3 3839 fundmen 4409 adjt 9773

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-sep 2693 ax-pow 2732 ax-pr 2769 ax-un 2857

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-rex 1642 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406 df-uni 2494 df-br 2610 df-opab 2657 df-id 2824 df-xp 3174 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-fv 3188