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 6751

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 6666	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5837	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6538	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6516	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6516	. 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 5637 Fun wfun 6505 ⟶wf 6507 –1-1→wf1 6508

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 2701

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 2708 df-cleq 2721 df-clel 2803 df-rab 3406 df-v 3449 df-dif 3917 df-un 3919 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516

This theorem is referenced by: f1oeq1 6788 f1eq123d 6792 fo00 6836 f1prex 7259 f1iun 7922 tposf12 8230 oacomf1olem 8528 f1dom4g 8937 f1dom3g 8939 f1domg 8943 dom3d 8965 domtr 8978 0domg 9068 domssex2 9101 1sdomOLD 9196 marypha1lem 9384 fseqenlem1 9977 dfac12lem2 10098 dfac12lem3 10099 ackbij2 10195 fin23lem28 10293 fin23lem32 10297 fin23lem34 10299 fin23lem35 10300 fin23lem41 10305 iundom2g 10493 pwfseqlem5 10616 hashf1lem1 14420 hashf1lem2 14421 hashf1 14422 4sqlem11 16926 injsubmefmnd 18824 conjsubgen 19183 sylow1lem2 19529 sylow2blem1 19550 hauspwpwf1 23874 istrkg2ld 28387 axlowdim 28888 sizusglecusg 29391 specval 31827 aciunf1lem 32586 zrhchr 33964 qqhre 34010 hashnexinj 42116 eldioph2lem2 42749 meadjiunlem 46463 fcoresf1b 47071 fundcmpsurbijinjpreimafv 47408 fundcmpsurinjpreimafv 47409 fundcmpsurinjimaid 47412 f1sn2g 48839 f102g 48840