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 6732

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 6647	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5829	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6521	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6504	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6504	. 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 5630 Fun wfun 6493 ⟶wf 6495 –1-1→wf1 6496

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 3391 df-v 3432 df-dif 3893 df-un 3895 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-br 5087 df-opab 5149 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504

This theorem is referenced by: f1oeq1 6769 f1eq123d 6773 fo00 6817 f1prex 7239 f1iun 7897 tposf12 8201 oacomf1olem 8499 f1dom4g 8912 f1dom3g 8914 f1domg 8918 dom3d 8941 domtr 8954 0domg 9042 domssex2 9075 marypha1lem 9346 fseqenlem1 9946 dfac12lem2 10067 dfac12lem3 10068 ackbij2 10164 fin23lem28 10262 fin23lem32 10266 fin23lem34 10268 fin23lem35 10269 fin23lem41 10274 iundom2g 10462 pwfseqlem5 10586 hashf1lem1 14417 hashf1lem2 14418 hashf1 14419 4sqlem11 16926 injsubmefmnd 18865 conjsubgen 19226 sylow1lem2 19574 sylow2blem1 19595 hauspwpwf1 23952 oldfib 28369 istrkg2ld 28528 axlowdim 29030 sizusglecusg 29532 specval 31969 aciunf1lem 32735 zrhchr 34118 qqhre 34164 hashnexinj 42567 eldioph2lem2 43193 meadjiunlem 46893 fcoresf1b 47512 fundcmpsurbijinjpreimafv 47861 fundcmpsurinjpreimafv 47862 fundcmpsurinjimaid 47865 f1sn2g 49320 f102g 49321