f1oeq3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1oeq3		Structured version Visualization version GIF version

Theorem f1oeq3 6825

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

**Assertion**
Ref	Expression
f1oeq3	⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

**Proof of Theorem f1oeq3**
Step	Hyp	Ref	Expression
1		f1eq3 6786	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6805	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6554	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6554	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 –1-1→wf1 6544 –onto→wfo 6545 –1-1-onto→wf1o 6546

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-9 2156 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1812 df-cleq 2755 df-ss 3901 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554

This theorem is used by: f1oeq23 6826 f1oeq123d 6829 f1oeq3d 6832 f1ores 6850 resin 6858 isoeq5 7339 breng 8996 xpcomf1o 9099 isinf 9270 cnfcom2 9716 fin1a2lem6 10496 pwfseqlem5 10761 pwfseq 10762 hashgf1o 14127 axdc4uzlem 14139 sumeq1 15871 prodeq1f 16090 prodeq1 16091 prodeq1i 16100 unbenlem 17101 4sqlem11 17148 gsumvalx 18880 cayley 19643 cayleyth 19644 ovolicc2lem4 25856 logf1o2 26993 uspgrf1oedg 29769 uspgredgiedg 29771 wlkiswwlks2lem4 30476 clwwlknonclwlknonf1o 30978 dlwwlknondlwlknonf1o 30981 adjbd1o 32702 rinvf1o 33281 cshf1o 33579 eulerpartgbij 35060 eulerpartlemgh 35066 derangval 36056 subfacp1lem2a 36069 subfacp1lem3 36071 subfacp1lem5 36073 mrsubff1o 36404 msubff1o 36446 cbvprodvw2 37169 bj-finsumval0 38352 f1omptsnlem 38405 f1omptsn 38406 poimirlem9 38693 poimirlem15 38699 ismtyval 38880 ismrer1 38918 lautset 41285 pautsetN 41301 hvmap1o2 42968 pwfi2f1o 44244 imasgim 44248 alephiso2 44705 f1ocof1ob2 48297 isuspgrim0lem 49136 gricushgr 49160 grtriprop 49184 grtrif1o 49185 isgrtri 49186 uspgrsprfo 49391