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 6811

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 6772	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6791	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6544	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6544	. 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

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-9 2159 ax-ext 2741

This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1807 df-cleq 2761 df-ss 3930 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544

This theorem is referenced by: f1oeq23 6812 f1oeq123d 6815 f1oeq3d 6818 f1ores 6836 resin 6844 isoeq5 7320 breng 8951 xpcomf1o 9053 isinf 9224 cnfcom2 9670 fin1a2lem6 10388 pwfseqlem5 10647 pwfseq 10648 hashgf1o 14006 axdc4uzlem 14018 sumeq1 15739 prodeq1f 15959 prodeq1 15960 prodeq1i 15969 unbenlem 16967 4sqlem11 17014 gsumvalx 18733 cayley 19483 cayleyth 19484 ovolicc2lem4 25647 logf1o2 26780 uspgrf1oedg 29463 uspgredgiedg 29465 wlkiswwlks2lem4 30161 clwwlknonclwlknonf1o 30653 dlwwlknondlwlknonf1o 30656 adjbd1o 32377 rinvf1o 32915 cshf1o 33222 eulerpartgbij 34706 eulerpartlemgh 34712 derangval 35557 subfacp1lem2a 35570 subfacp1lem3 35572 subfacp1lem5 35574 mrsubff1o 35905 msubff1o 35947 cbvprodvw2 36647 bj-finsumval0 37816 f1omptsnlem 37869 f1omptsn 37870 poimirlem9 38167 poimirlem15 38173 ismtyval 38338 ismrer1 38376 lautset 40745 pautsetN 40761 hvmap1o2 42428 pwfi2f1o 43714 imasgim 43718 alephiso2 44175 f1ocof1ob2 47707 isuspgrim0lem 48546 gricushgr 48570 grtriprop 48594 grtrif1o 48595 isgrtri 48596 uspgrsprfo 48801