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 6553

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 6477	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5711	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6355	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 634	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6338	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6338	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 318	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1539 ^◡ccnv 5521 Fun wfun 6327 ⟶wf 6329 –1-1→wf1 6330

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2730

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-ex 1783 df-sb 2071 df-clab 2737 df-cleq 2751 df-clel 2831 df-v 3412 df-un 3864 df-in 3866 df-ss 3876 df-sn 4521 df-pr 4523 df-op 4527 df-br 5031 df-opab 5093 df-rel 5529 df-cnv 5530 df-co 5531 df-dm 5532 df-rn 5533 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338

This theorem is referenced by: f1oeq1 6588 f1eq123d 6592 fo00 6635 f1prex 7030 f1iun 7647 tposf12 7925 oacomf1olem 8198 f1dom2g 8543 f1domg 8545 dom3d 8567 domtr 8578 domssex2 8696 1sdom 8740 marypha1lem 8920 fseqenlem1 9474 dfac12lem2 9594 dfac12lem3 9595 ackbij2 9693 fin23lem28 9790 fin23lem32 9794 fin23lem34 9796 fin23lem35 9797 fin23lem41 9802 iundom2g 9990 pwfseqlem5 10113 hashf1lem1 13854 hashf1lem1OLD 13855 hashf1lem2 13856 hashf1 13857 4sqlem11 16336 injsubmefmnd 18118 conjsubgen 18448 sylow1lem2 18781 sylow2blem1 18802 hauspwpwf1 22677 istrkg2ld 26343 axlowdim 26844 sizusglecusg 27342 specval 29770 aciunf1lem 30513 zrhchr 31435 qqhre 31479 eldioph2lem2 40065 meadjiunlem 43460 fundcmpsurbijinjpreimafv 44282 fundcmpsurinjpreimafv 44283 fundcmpsurinjimaid 44286