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 6733

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 6648	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5830	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6522	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6505	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6505	. 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 1542 ^◡ccnv 5631 Fun wfun 6494 ⟶wf 6496 –1-1→wf1 6497

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505

This theorem is referenced by: f1oeq1 6770 f1eq123d 6774 fo00 6818 f1prex 7240 f1iun 7898 tposf12 8203 oacomf1olem 8501 f1dom4g 8914 f1dom3g 8916 f1domg 8920 dom3d 8943 domtr 8956 0domg 9044 domssex2 9077 marypha1lem 9348 fseqenlem1 9946 dfac12lem2 10067 dfac12lem3 10068 ackbij2 10164 fin23lem28 10262 fin23lem32 10266 fin23lem34 10268 fin23lem35 10269 fin23lem41 10274 iundom2g 10462 pwfseqlem5 10586 hashf1lem1 14390 hashf1lem2 14391 hashf1 14392 4sqlem11 16895 injsubmefmnd 18834 conjsubgen 19192 sylow1lem2 19540 sylow2blem1 19561 hauspwpwf1 23943 oldfib 28385 istrkg2ld 28544 axlowdim 29046 sizusglecusg 29549 specval 31986 aciunf1lem 32752 zrhchr 34152 qqhre 34198 hashnexinj 42498 eldioph2lem2 43118 meadjiunlem 46823 fcoresf1b 47430 fundcmpsurbijinjpreimafv 47767 fundcmpsurinjpreimafv 47768 fundcmpsurinjimaid 47771 f1sn2g 49210 f102g 49211