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 6725

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 6640	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5822	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6514	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6497	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6497	. 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 5623 Fun wfun 6486 ⟶wf 6488 –1-1→wf1 6489

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 2708

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 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497

This theorem is referenced by: f1oeq1 6762 f1eq123d 6766 fo00 6810 f1prex 7230 f1iun 7888 tposf12 8193 oacomf1olem 8491 f1dom4g 8902 f1dom3g 8904 f1domg 8908 dom3d 8931 domtr 8944 0domg 9032 domssex2 9065 marypha1lem 9336 fseqenlem1 9934 dfac12lem2 10055 dfac12lem3 10056 ackbij2 10152 fin23lem28 10250 fin23lem32 10254 fin23lem34 10256 fin23lem35 10257 fin23lem41 10262 iundom2g 10450 pwfseqlem5 10574 hashf1lem1 14378 hashf1lem2 14379 hashf1 14380 4sqlem11 16883 injsubmefmnd 18822 conjsubgen 19180 sylow1lem2 19528 sylow2blem1 19549 hauspwpwf1 23931 oldfib 28373 istrkg2ld 28532 axlowdim 29034 sizusglecusg 29537 specval 31973 aciunf1lem 32740 zrhchr 34131 qqhre 34177 hashnexinj 42382 eldioph2lem2 43003 meadjiunlem 46709 fcoresf1b 47316 fundcmpsurbijinjpreimafv 47653 fundcmpsurinjpreimafv 47654 fundcmpsurinjimaid 47657 f1sn2g 49096 f102g 49097