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 6799

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 6716	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5886	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6589	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6567	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6567	. 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 1536 ^◡ccnv 5687 Fun wfun 6556 ⟶wf 6558 –1-1→wf1 6559

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567

This theorem is referenced by: f1oeq1 6836 f1eq123d 6840 fo00 6884 f1prex 7303 f1iun 7966 tposf12 8274 oacomf1olem 8600 f1dom4g 9004 f1dom3g 9006 f1domg 9010 dom3d 9032 domtr 9045 0domg 9138 domssex2 9175 1sdomOLD 9282 marypha1lem 9470 fseqenlem1 10061 dfac12lem2 10182 dfac12lem3 10183 ackbij2 10279 fin23lem28 10377 fin23lem32 10381 fin23lem34 10383 fin23lem35 10384 fin23lem41 10389 iundom2g 10577 pwfseqlem5 10700 hashf1lem1 14490 hashf1lem2 14491 hashf1 14492 4sqlem11 16988 injsubmefmnd 18922 conjsubgen 19281 sylow1lem2 19631 sylow2blem1 19652 hauspwpwf1 24010 istrkg2ld 28482 axlowdim 28990 sizusglecusg 29495 specval 31926 aciunf1lem 32678 zrhchr 33936 qqhre 33982 hashnexinj 42109 eldioph2lem2 42748 meadjiunlem 46420 fcoresf1b 47019 fundcmpsurbijinjpreimafv 47331 fundcmpsurinjpreimafv 47332 fundcmpsurinjimaid 47335 f1sn2g 48680 f102g 48681