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 6783

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 6699	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5874	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6571	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6549	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6549	. 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 205 ∧ wa 397 = wceq 1542 ^◡ccnv 5676 Fun wfun 6538 ⟶wf 6540 –1-1→wf1 6541

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549

This theorem is referenced by: f1oeq1 6822 f1eq123d 6826 fo00 6870 f1prex 7282 f1iun 7930 tposf12 8236 oacomf1olem 8564 f1dom4g 8961 f1dom3g 8963 f1dom2gOLD 8966 f1domg 8968 dom3d 8990 domtr 9003 0domg 9100 domssex2 9137 1sdomOLD 9249 marypha1lem 9428 fseqenlem1 10019 dfac12lem2 10139 dfac12lem3 10140 ackbij2 10238 fin23lem28 10335 fin23lem32 10339 fin23lem34 10341 fin23lem35 10342 fin23lem41 10347 iundom2g 10535 pwfseqlem5 10658 hashf1lem1 14415 hashf1lem1OLD 14416 hashf1lem2 14417 hashf1 14418 4sqlem11 16888 injsubmefmnd 18778 conjsubgen 19125 sylow1lem2 19467 sylow2blem1 19488 hauspwpwf1 23491 istrkg2ld 27711 axlowdim 28219 sizusglecusg 28720 specval 31151 aciunf1lem 31887 zrhchr 32956 qqhre 33000 eldioph2lem2 41499 meadjiunlem 45181 fcoresf1b 45780 fundcmpsurbijinjpreimafv 46075 fundcmpsurinjpreimafv 46076 fundcmpsurinjimaid 46079 f1sn2g 47517 f102g 47518