f1eq1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1eq1		Structured version Visualization version GIF version

Theorem f1eq1 6695

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)

**Assertion**
Ref	Expression
f1eq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

**Proof of Theorem f1eq1**
Step	Hyp	Ref	Expression
1		feq1 6611	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5795	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6485	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6463	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6463	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1539 ^◡ccnv 5599 Fun wfun 6452 ⟶wf 6454 –1-1→wf1 6455

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2707

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3306 df-v 3439 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4566 df-pr 4568 df-op 4572 df-br 5082 df-opab 5144 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463

This theorem is referenced by: f1oeq1 6734 f1eq123d 6738 fo00 6782 f1prex 7188 f1iun 7818 tposf12 8098 oacomf1olem 8426 f1dom4g 8786 f1dom3g 8788 f1dom2gOLD 8791 f1domg 8793 dom3d 8815 domtr 8828 0domg 8925 domssex2 8962 1sdomOLD 9070 marypha1lem 9240 fseqenlem1 9830 dfac12lem2 9950 dfac12lem3 9951 ackbij2 10049 fin23lem28 10146 fin23lem32 10150 fin23lem34 10152 fin23lem35 10153 fin23lem41 10158 iundom2g 10346 pwfseqlem5 10469 hashf1lem1 14217 hashf1lem1OLD 14218 hashf1lem2 14219 hashf1 14220 4sqlem11 16705 injsubmefmnd 18585 conjsubgen 18916 sylow1lem2 19253 sylow2blem1 19274 hauspwpwf1 23187 istrkg2ld 26870 axlowdim 27378 sizusglecusg 27879 specval 30309 aciunf1lem 31048 zrhchr 31975 qqhre 32019 eldioph2lem2 40778 meadjiunlem 44233 fcoresf1b 44808 fundcmpsurbijinjpreimafv 45103 fundcmpsurinjpreimafv 45104 fundcmpsurinjimaid 45107 f1sn2g 46422 f102g 46423