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 6726

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 6641	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5823	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6515	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6498	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6498	. 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 5624 Fun wfun 6487 ⟶wf 6489 –1-1→wf1 6490

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 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498

This theorem is referenced by: f1oeq1 6763 f1eq123d 6767 fo00 6811 f1prex 7233 f1iun 7891 tposf12 8195 oacomf1olem 8493 f1dom4g 8906 f1dom3g 8908 f1domg 8912 dom3d 8935 domtr 8948 0domg 9036 domssex2 9069 marypha1lem 9340 fseqenlem1 9940 dfac12lem2 10061 dfac12lem3 10062 ackbij2 10158 fin23lem28 10256 fin23lem32 10260 fin23lem34 10262 fin23lem35 10263 fin23lem41 10268 iundom2g 10456 pwfseqlem5 10580 hashf1lem1 14411 hashf1lem2 14412 hashf1 14413 4sqlem11 16920 injsubmefmnd 18859 conjsubgen 19220 sylow1lem2 19568 sylow2blem1 19589 hauspwpwf1 23965 oldfib 28386 istrkg2ld 28545 axlowdim 29047 sizusglecusg 29550 specval 31987 aciunf1lem 32753 zrhchr 34137 qqhre 34183 hashnexinj 42584 eldioph2lem2 43210 meadjiunlem 46914 fcoresf1b 47533 fundcmpsurbijinjpreimafv 47882 fundcmpsurinjpreimafv 47883 fundcmpsurinjimaid 47886 f1sn2g 49341 f102g 49342