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 6573

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 6498	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5747	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6380	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6363	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6363	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ^◡ccnv 5557 Fun wfun 6352 ⟶wf 6354 –1-1→wf1 6355

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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-br 5070 df-opab 5132 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363

This theorem is referenced by: f1oeq1 6607 f1eq123d 6611 fo00 6653 f1prex 7043 f1iun 7648 tposf12 7920 oacomf1olem 8193 f1dom2g 8530 f1domg 8532 dom3d 8554 domtr 8565 domssex2 8680 1sdom 8724 marypha1lem 8900 fseqenlem1 9453 dfac12lem2 9573 dfac12lem3 9574 ackbij2 9668 fin23lem28 9765 fin23lem32 9769 fin23lem34 9771 fin23lem35 9772 fin23lem41 9777 iundom2g 9965 pwfseqlem5 10088 hashf1lem1 13816 hashf1lem2 13817 hashf1 13818 4sqlem11 16294 injsubmefmnd 18065 conjsubgen 18394 sylow1lem2 18727 sylow2blem1 18748 hauspwpwf1 22598 istrkg2ld 26249 axlowdim 26750 sizusglecusg 27248 specval 29678 aciunf1lem 30410 zrhchr 31221 qqhre 31265 eldioph2lem2 39364 meadjiunlem 42754 fundcmpsurbijinjpreimafv 43574 fundcmpsurinjpreimafv 43575 fundcmpsurinjimaid 43578