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 6731

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 6646	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5828	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6520	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6503	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6503	. 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 1542 ^◡ccnv 5630 Fun wfun 6492 ⟶wf 6494 –1-1→wf1 6495

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3390 df-v 3431 df-dif 3892 df-un 3894 df-ss 3906 df-nul 4274 df-if 4467 df-sn 4568 df-pr 4570 df-op 4574 df-br 5086 df-opab 5148 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503

This theorem is referenced by: f1oeq1 6768 f1eq123d 6772 fo00 6816 f1prex 7239 f1iun 7897 tposf12 8201 oacomf1olem 8499 f1dom4g 8912 f1dom3g 8914 f1domg 8918 dom3d 8941 domtr 8954 0domg 9042 domssex2 9075 marypha1lem 9346 fseqenlem1 9946 dfac12lem2 10067 dfac12lem3 10068 ackbij2 10164 fin23lem28 10262 fin23lem32 10266 fin23lem34 10268 fin23lem35 10269 fin23lem41 10274 iundom2g 10462 pwfseqlem5 10586 hashf1lem1 14417 hashf1lem2 14418 hashf1 14419 4sqlem11 16926 injsubmefmnd 18865 conjsubgen 19226 sylow1lem2 19574 sylow2blem1 19595 hauspwpwf1 23952 oldfib 28369 istrkg2ld 28528 axlowdim 29030 sizusglecusg 29532 specval 31969 aciunf1lem 32735 zrhchr 34118 qqhre 34164 hashnexinj 42567 eldioph2lem2 43193 meadjiunlem 46893 fcoresf1b 47518 fundcmpsurbijinjpreimafv 47867 fundcmpsurinjpreimafv 47868 fundcmpsurinjimaid 47871 f1sn2g 49326 f102g 49327