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 6710

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 6626	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5809	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6500	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6478	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6478	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ^◡ccnv 5613 Fun wfun 6467 ⟶wf 6469 –1-1→wf1 6470

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2707

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3404 df-v 3443 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4269 df-if 4473 df-sn 4573 df-pr 4575 df-op 4579 df-br 5090 df-opab 5152 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-fun 6475 df-fn 6476 df-f 6477 df-f1 6478

This theorem is referenced by: f1oeq1 6749 f1eq123d 6753 fo00 6797 f1prex 7206 f1iun 7846 tposf12 8129 oacomf1olem 8458 f1dom4g 8818 f1dom3g 8820 f1dom2gOLD 8823 f1domg 8825 dom3d 8847 domtr 8860 0domg 8957 domssex2 8994 1sdomOLD 9106 marypha1lem 9282 fseqenlem1 9873 dfac12lem2 9993 dfac12lem3 9994 ackbij2 10092 fin23lem28 10189 fin23lem32 10193 fin23lem34 10195 fin23lem35 10196 fin23lem41 10201 iundom2g 10389 pwfseqlem5 10512 hashf1lem1 14260 hashf1lem1OLD 14261 hashf1lem2 14262 hashf1 14263 4sqlem11 16745 injsubmefmnd 18624 conjsubgen 18955 sylow1lem2 19292 sylow2blem1 19313 hauspwpwf1 23236 istrkg2ld 27023 axlowdim 27531 sizusglecusg 28032 specval 30461 aciunf1lem 31199 zrhchr 32137 qqhre 32181 eldioph2lem2 40833 meadjiunlem 44329 fcoresf1b 44904 fundcmpsurbijinjpreimafv 45199 fundcmpsurinjpreimafv 45200 fundcmpsurinjimaid 45203 f1sn2g 46518 f102g 46519