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 6754

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 6669	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5840	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6541	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6519	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6519	. 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 1540 ^◡ccnv 5640 Fun wfun 6508 ⟶wf 6510 –1-1→wf1 6511

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2702

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-ss 3934 df-nul 4300 df-if 4492 df-sn 4593 df-pr 4595 df-op 4599 df-br 5111 df-opab 5173 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519

This theorem is referenced by: f1oeq1 6791 f1eq123d 6795 fo00 6839 f1prex 7262 f1iun 7925 tposf12 8233 oacomf1olem 8531 f1dom4g 8940 f1dom3g 8942 f1domg 8946 dom3d 8968 domtr 8981 0domg 9074 domssex2 9107 1sdomOLD 9203 marypha1lem 9391 fseqenlem1 9984 dfac12lem2 10105 dfac12lem3 10106 ackbij2 10202 fin23lem28 10300 fin23lem32 10304 fin23lem34 10306 fin23lem35 10307 fin23lem41 10312 iundom2g 10500 pwfseqlem5 10623 hashf1lem1 14427 hashf1lem2 14428 hashf1 14429 4sqlem11 16933 injsubmefmnd 18831 conjsubgen 19190 sylow1lem2 19536 sylow2blem1 19557 hauspwpwf1 23881 istrkg2ld 28394 axlowdim 28895 sizusglecusg 29398 specval 31834 aciunf1lem 32593 zrhchr 33971 qqhre 34017 hashnexinj 42123 eldioph2lem2 42756 meadjiunlem 46470 fcoresf1b 47075 fundcmpsurbijinjpreimafv 47412 fundcmpsurinjpreimafv 47413 fundcmpsurinjimaid 47416 f1sn2g 48843 f102g 48844