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 6779

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 6740	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6759	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6508	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6508	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 –1-1→wf1 6498 –onto→wfo 6499 –1-1-onto→wf1o 6500

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702

This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3448 df-in 3920 df-ss 3930 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508

This theorem is referenced by: f1oeq23 6780 f1oeq123d 6783 f1oeq3d 6786 f1ores 6803 resin 6811 isoeq5 7271 breng 8899 brenOLD 8901 xpcomf1o 9012 isinf 9211 isinfOLD 9212 cnfcom2 9647 fin1a2lem6 10350 pwfseqlem5 10608 pwfseq 10609 hashgf1o 13886 axdc4uzlem 13898 sumeq1 15585 prodeq1f 15802 unbenlem 16791 4sqlem11 16838 gsumvalx 18545 cayley 19210 cayleyth 19211 ovolicc2lem4 24921 logf1o2 26042 uspgrf1oedg 28187 wlkiswwlks2lem4 28880 clwwlknonclwlknonf1o 29369 dlwwlknondlwlknonf1o 29372 adjbd1o 31090 rinvf1o 31611 cshf1o 31886 eulerpartgbij 33061 eulerpartlemgh 33067 derangval 33848 subfacp1lem2a 33861 subfacp1lem3 33863 subfacp1lem5 33865 mrsubff1o 34196 msubff1o 34238 bj-finsumval0 35829 f1omptsnlem 35880 f1omptsn 35881 poimirlem9 36160 poimirlem15 36166 ismtyval 36332 ismrer1 36370 lautset 38618 pautsetN 38634 hvmap1o2 40301 pwfi2f1o 41481 imasgim 41485 alephiso2 41952 f1ocof1ob2 45434 isomushgr 46138 uspgrsprfo 46170