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 6768

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 6685	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5853	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6557	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6535	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6535	. 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 5653 Fun wfun 6524 ⟶wf 6526 –1-1→wf1 6527

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 2007 ax-8 2110 ax-9 2118 ax-ext 2707

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 2065 df-clab 2714 df-cleq 2727 df-clel 2809 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-br 5120 df-opab 5182 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535

This theorem is referenced by: f1oeq1 6805 f1eq123d 6809 fo00 6853 f1prex 7276 f1iun 7940 tposf12 8248 oacomf1olem 8574 f1dom4g 8978 f1dom3g 8980 f1domg 8984 dom3d 9006 domtr 9019 0domg 9112 domssex2 9149 1sdomOLD 9255 marypha1lem 9443 fseqenlem1 10036 dfac12lem2 10157 dfac12lem3 10158 ackbij2 10254 fin23lem28 10352 fin23lem32 10356 fin23lem34 10358 fin23lem35 10359 fin23lem41 10364 iundom2g 10552 pwfseqlem5 10675 hashf1lem1 14471 hashf1lem2 14472 hashf1 14473 4sqlem11 16973 injsubmefmnd 18873 conjsubgen 19232 sylow1lem2 19578 sylow2blem1 19599 hauspwpwf1 23923 istrkg2ld 28385 axlowdim 28886 sizusglecusg 29389 specval 31825 aciunf1lem 32586 zrhchr 33951 qqhre 33997 hashnexinj 42087 eldioph2lem2 42731 meadjiunlem 46442 fcoresf1b 47047 fundcmpsurbijinjpreimafv 47369 fundcmpsurinjpreimafv 47370 fundcmpsurinjimaid 47373 f1sn2g 48777 f102g 48778