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 6714

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 6629	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5812	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6503	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6486	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6486	. 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 1541 ^◡ccnv 5613 Fun wfun 6475 ⟶wf 6477 –1-1→wf1 6478

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 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-br 5090 df-opab 5152 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486

This theorem is referenced by: f1oeq1 6751 f1eq123d 6755 fo00 6799 f1prex 7218 f1iun 7876 tposf12 8181 oacomf1olem 8479 f1dom4g 8888 f1dom3g 8890 f1domg 8894 dom3d 8916 domtr 8929 0domg 9017 domssex2 9050 marypha1lem 9317 fseqenlem1 9915 dfac12lem2 10036 dfac12lem3 10037 ackbij2 10133 fin23lem28 10231 fin23lem32 10235 fin23lem34 10237 fin23lem35 10238 fin23lem41 10243 iundom2g 10431 pwfseqlem5 10554 hashf1lem1 14362 hashf1lem2 14363 hashf1 14364 4sqlem11 16867 injsubmefmnd 18805 conjsubgen 19163 sylow1lem2 19511 sylow2blem1 19532 hauspwpwf1 23902 istrkg2ld 28438 axlowdim 28939 sizusglecusg 29442 specval 31878 aciunf1lem 32644 zrhchr 33987 qqhre 34033 hashnexinj 42169 eldioph2lem2 42802 meadjiunlem 46511 fcoresf1b 47109 fundcmpsurbijinjpreimafv 47446 fundcmpsurinjpreimafv 47447 fundcmpsurinjimaid 47450 f1sn2g 48890 f102g 48891