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 6738

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 6654	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5834	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6528	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6506	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6506	. 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 1541 ^◡ccnv 5637 Fun wfun 6495 ⟶wf 6497 –1-1→wf1 6498

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506

This theorem is referenced by: f1oeq1 6777 f1eq123d 6781 fo00 6825 f1prex 7235 f1iun 7881 tposf12 8187 oacomf1olem 8516 f1dom4g 8912 f1dom3g 8914 f1dom2gOLD 8917 f1domg 8919 dom3d 8941 domtr 8954 0domg 9051 domssex2 9088 1sdomOLD 9200 marypha1lem 9378 fseqenlem1 9969 dfac12lem2 10089 dfac12lem3 10090 ackbij2 10188 fin23lem28 10285 fin23lem32 10289 fin23lem34 10291 fin23lem35 10292 fin23lem41 10297 iundom2g 10485 pwfseqlem5 10608 hashf1lem1 14365 hashf1lem1OLD 14366 hashf1lem2 14367 hashf1 14368 4sqlem11 16838 injsubmefmnd 18721 conjsubgen 19055 sylow1lem2 19395 sylow2blem1 19416 hauspwpwf1 23375 istrkg2ld 27465 axlowdim 27973 sizusglecusg 28474 specval 30903 aciunf1lem 31645 zrhchr 32646 qqhre 32690 eldioph2lem2 41142 meadjiunlem 44826 fcoresf1b 45424 fundcmpsurbijinjpreimafv 45719 fundcmpsurinjpreimafv 45720 fundcmpsurinjimaid 45723 f1sn2g 47037 f102g 47038