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 6718

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 6633	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5815	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6507	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 638	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6490	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6490	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ^◡ccnv 5617 Fun wfun 6479 ⟶wf 6481 –1-1→wf1 6482

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2711

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2718 df-cleq 2731 df-clel 2814 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-ss 3900 df-nul 4262 df-if 4455 df-sn 4556 df-pr 4558 df-op 4562 df-br 5073 df-opab 5135 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490

This theorem is referenced by: f1oeq1 6755 f1eq123d 6759 fo00 6803 f1prex 7228 f1iun 7886 tposf12 8191 oacomf1olem 8489 f1dom4g 8902 f1dom3g 8904 f1domg 8908 dom3d 8931 domtr 8944 0domg 9032 domssex2 9065 marypha1lem 9336 fseqenlem1 9937 dfac12lem2 10058 dfac12lem3 10059 ackbij2 10155 fin23lem28 10253 fin23lem32 10257 fin23lem34 10259 fin23lem35 10260 fin23lem41 10265 iundom2g 10453 pwfseqlem5 10577 hashf1lem1 14408 hashf1lem2 14409 hashf1 14410 4sqlem11 16917 injsubmefmnd 18856 conjsubgen 19217 sylow1lem2 19565 sylow2blem1 19586 hauspwpwf1 23970 oldfib 28387 istrkg2ld 28546 axlowdim 29048 sizusglecusg 29550 specval 31987 aciunf1lem 32754 zrhchr 34158 qqhre 34204 hashnexinj 42613 eldioph2lem2 43210 meadjiunlem 46908 fcoresf1b 47533 fundcmpsurbijinjpreimafv 47882 fundcmpsurinjpreimafv 47883 fundcmpsurinjimaid 47886 f1sn2g 49341 f102g 49342