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 6733

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 6648	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5827	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6522	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6504	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6504	. 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 206 ∧ wa 395 = wceq 1540 ^◡ccnv 5630 Fun wfun 6493 ⟶wf 6495 –1-1→wf1 6496

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 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-br 5103 df-opab 5165 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504

This theorem is referenced by: f1oeq1 6770 f1eq123d 6774 fo00 6818 f1prex 7241 f1iun 7902 tposf12 8207 oacomf1olem 8505 f1dom4g 8914 f1dom3g 8916 f1domg 8920 dom3d 8942 domtr 8955 0domg 9045 domssex2 9078 1sdomOLD 9172 marypha1lem 9360 fseqenlem1 9953 dfac12lem2 10074 dfac12lem3 10075 ackbij2 10171 fin23lem28 10269 fin23lem32 10273 fin23lem34 10275 fin23lem35 10276 fin23lem41 10281 iundom2g 10469 pwfseqlem5 10592 hashf1lem1 14396 hashf1lem2 14397 hashf1 14398 4sqlem11 16902 injsubmefmnd 18800 conjsubgen 19159 sylow1lem2 19505 sylow2blem1 19526 hauspwpwf1 23850 istrkg2ld 28363 axlowdim 28864 sizusglecusg 29367 specval 31800 aciunf1lem 32559 zrhchr 33937 qqhre 33983 hashnexinj 42089 eldioph2lem2 42722 meadjiunlem 46436 fcoresf1b 47044 fundcmpsurbijinjpreimafv 47381 fundcmpsurinjpreimafv 47382 fundcmpsurinjimaid 47385 f1sn2g 48812 f102g 48813