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 6810

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 6771	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6790	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6543	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6543	. 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 400 = wceq 1570 –1-1→wf1 6533 –onto→wfo 6534 –1-1-onto→wf1o 6535

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-9 2153 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 401 df-ex 1810 df-cleq 2755 df-ss 3922 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543

This theorem is used by: f1oeq23 6811 f1oeq123d 6814 f1oeq3d 6817 f1ores 6835 resin 6843 isoeq5 7319 breng 8948 xpcomf1o 9050 isinf 9221 cnfcom2 9667 fin1a2lem6 10393 pwfseqlem5 10652 pwfseq 10653 hashgf1o 14012 axdc4uzlem 14024 sumeq1 15745 prodeq1f 15965 prodeq1 15966 prodeq1i 15975 unbenlem 16972 4sqlem11 17019 gsumvalx 18738 cayley 19488 cayleyth 19489 ovolicc2lem4 25688 logf1o2 26824 uspgrf1oedg 29532 uspgredgiedg 29534 wlkiswwlks2lem4 30230 clwwlknonclwlknonf1o 30722 dlwwlknondlwlknonf1o 30725 adjbd1o 32446 rinvf1o 32984 cshf1o 33291 eulerpartgbij 34771 eulerpartlemgh 34777 derangval 35667 subfacp1lem2a 35680 subfacp1lem3 35682 subfacp1lem5 35684 mrsubff1o 36015 msubff1o 36057 cbvprodvw2 36787 bj-finsumval0 37957 f1omptsnlem 38010 f1omptsn 38011 poimirlem9 38308 poimirlem15 38314 ismtyval 38479 ismrer1 38517 lautset 40884 pautsetN 40900 hvmap1o2 42567 pwfi2f1o 43851 imasgim 43855 alephiso2 44312 f1ocof1ob2 47847 isuspgrim0lem 48686 gricushgr 48710 grtriprop 48734 grtrif1o 48735 isgrtri 48736 uspgrsprfo 48941