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 6812

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 6728	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5898	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6600	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6578	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6578	. 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 1537 ^◡ccnv 5699 Fun wfun 6567 ⟶wf 6569 –1-1→wf1 6570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-br 5167 df-opab 5229 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578

This theorem is referenced by: f1oeq1 6850 f1eq123d 6854 fo00 6898 f1prex 7320 f1iun 7984 tposf12 8292 oacomf1olem 8620 f1dom4g 9025 f1dom3g 9027 f1dom2gOLD 9030 f1domg 9032 dom3d 9054 domtr 9067 0domg 9166 domssex2 9203 1sdomOLD 9312 marypha1lem 9502 fseqenlem1 10093 dfac12lem2 10214 dfac12lem3 10215 ackbij2 10311 fin23lem28 10409 fin23lem32 10413 fin23lem34 10415 fin23lem35 10416 fin23lem41 10421 iundom2g 10609 pwfseqlem5 10732 hashf1lem1 14504 hashf1lem2 14505 hashf1 14506 4sqlem11 17002 injsubmefmnd 18932 conjsubgen 19291 sylow1lem2 19641 sylow2blem1 19662 hauspwpwf1 24016 istrkg2ld 28486 axlowdim 28994 sizusglecusg 29499 specval 31930 aciunf1lem 32680 zrhchr 33922 qqhre 33966 hashnexinj 42085 eldioph2lem2 42717 meadjiunlem 46386 fcoresf1b 46985 fundcmpsurbijinjpreimafv 47281 fundcmpsurinjpreimafv 47282 fundcmpsurinjimaid 47285 f1sn2g 48564 f102g 48565