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 6723

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 6638	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5820	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6512	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6495	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6495	. 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 5621 Fun wfun 6484 ⟶wf 6486 –1-1→wf1 6487

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 2115 ax-9 2123 ax-ext 2706

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 2713 df-cleq 2726 df-clel 2809 df-rab 3398 df-v 3440 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4284 df-if 4478 df-sn 4579 df-pr 4581 df-op 4585 df-br 5097 df-opab 5159 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495

This theorem is referenced by: f1oeq1 6760 f1eq123d 6764 fo00 6808 f1prex 7228 f1iun 7886 tposf12 8191 oacomf1olem 8489 f1dom4g 8900 f1dom3g 8902 f1domg 8906 dom3d 8929 domtr 8942 0domg 9030 domssex2 9063 marypha1lem 9334 fseqenlem1 9932 dfac12lem2 10053 dfac12lem3 10054 ackbij2 10150 fin23lem28 10248 fin23lem32 10252 fin23lem34 10254 fin23lem35 10255 fin23lem41 10260 iundom2g 10448 pwfseqlem5 10572 hashf1lem1 14376 hashf1lem2 14377 hashf1 14378 4sqlem11 16881 injsubmefmnd 18820 conjsubgen 19178 sylow1lem2 19526 sylow2blem1 19547 hauspwpwf1 23929 oldfib 28335 istrkg2ld 28481 axlowdim 28983 sizusglecusg 29486 specval 31922 aciunf1lem 32689 zrhchr 34080 qqhre 34126 hashnexinj 42321 eldioph2lem2 42945 meadjiunlem 46651 fcoresf1b 47258 fundcmpsurbijinjpreimafv 47595 fundcmpsurinjpreimafv 47596 fundcmpsurinjimaid 47599 f1sn2g 49038 f102g 49039