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 6779

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 6696	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5864	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6568	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6546	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6546	. 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 1539 ^◡ccnv 5664 Fun wfun 6535 ⟶wf 6537 –1-1→wf1 6538

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2706

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2713 df-cleq 2726 df-clel 2808 df-rab 3420 df-v 3465 df-dif 3934 df-un 3936 df-ss 3948 df-nul 4314 df-if 4506 df-sn 4607 df-pr 4609 df-op 4613 df-br 5124 df-opab 5186 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546

This theorem is referenced by: f1oeq1 6816 f1eq123d 6820 fo00 6864 f1prex 7286 f1iun 7950 tposf12 8258 oacomf1olem 8584 f1dom4g 8988 f1dom3g 8990 f1domg 8994 dom3d 9016 domtr 9029 0domg 9122 domssex2 9159 1sdomOLD 9267 marypha1lem 9455 fseqenlem1 10046 dfac12lem2 10167 dfac12lem3 10168 ackbij2 10264 fin23lem28 10362 fin23lem32 10366 fin23lem34 10368 fin23lem35 10369 fin23lem41 10374 iundom2g 10562 pwfseqlem5 10685 hashf1lem1 14477 hashf1lem2 14478 hashf1 14479 4sqlem11 16976 injsubmefmnd 18880 conjsubgen 19239 sylow1lem2 19586 sylow2blem1 19607 hauspwpwf1 23942 istrkg2ld 28405 axlowdim 28907 sizusglecusg 29410 specval 31846 aciunf1lem 32608 zrhchr 33950 qqhre 33996 hashnexinj 42104 eldioph2lem2 42750 meadjiunlem 46452 fcoresf1b 47055 fundcmpsurbijinjpreimafv 47367 fundcmpsurinjpreimafv 47368 fundcmpsurinjimaid 47371 f1sn2g 48737 f102g 48738