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 6433

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 6399	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6415	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 622	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6193	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6193	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 306	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1508 –1-1→wf1 6183 –onto→wfo 6184 –1-1-onto→wf1o 6185

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-in 3831 df-ss 3838 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193

This theorem is referenced by: f1oeq23 6434 f1oeq123d 6437 f1oeq3d 6439 f1ores 6456 resin 6463 isoeq5 6896 ncanth 6934 bren 8314 xpcomf1o 8401 isinf 8525 cnfcom2 8958 fin1a2lem6 9624 pwfseqlem5 9882 pwfseq 9883 hashgf1o 13153 axdc4uzlem 13165 sumeq1 14905 prodeq1f 15121 unbenlem 16099 4sqlem11 16146 gsumvalx 17751 cayley 18316 cayleyth 18317 ovolicc2lem4 23840 logf1o2 24950 uspgrf1oedg 26677 wlkiswwlks2lem4 27374 clwwlknonclwlknonf1o 27926 clwwlknonclwlknonf1oOLD 27927 dlwwlknondlwlknonf1o 27932 dlwwlknondlwlknonf1oOLD 27933 adjbd1o 29659 rinvf1o 30156 eulerpartgbij 31308 eulerpartlemgh 31314 derangval 32032 subfacp1lem2a 32045 subfacp1lem3 32047 subfacp1lem5 32049 mrsubff1o 32315 msubff1o 32357 bj-finsumval0 34063 f1omptsnlem 34092 f1omptsn 34093 poimirlem4 34370 poimirlem9 34375 poimirlem15 34381 ismtyval 34553 ismrer1 34591 lautset 36696 pautsetN 36712 hvmap1o2 38379 pwfi2f1o 39126 imasgim 39130 isomushgr 43389 uspgrsprfo 43421