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 6824

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 6785	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6804	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6551	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6551	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 –1-1→wf1 6541 –onto→wfo 6542 –1-1-onto→wf1o 6543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704

This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551

This theorem is referenced by: f1oeq23 6825 f1oeq123d 6828 f1oeq3d 6831 f1ores 6848 resin 6856 isoeq5 7318 breng 8948 brenOLD 8950 xpcomf1o 9061 isinf 9260 isinfOLD 9261 cnfcom2 9697 fin1a2lem6 10400 pwfseqlem5 10658 pwfseq 10659 hashgf1o 13936 axdc4uzlem 13948 sumeq1 15635 prodeq1f 15852 unbenlem 16841 4sqlem11 16888 gsumvalx 18595 cayley 19282 cayleyth 19283 ovolicc2lem4 25037 logf1o2 26158 uspgrf1oedg 28464 wlkiswwlks2lem4 29157 clwwlknonclwlknonf1o 29646 dlwwlknondlwlknonf1o 29649 adjbd1o 31369 rinvf1o 31885 cshf1o 32157 eulerpartgbij 33402 eulerpartlemgh 33408 derangval 34189 subfacp1lem2a 34202 subfacp1lem3 34204 subfacp1lem5 34206 mrsubff1o 34537 msubff1o 34579 bj-finsumval0 36214 f1omptsnlem 36265 f1omptsn 36266 poimirlem9 36545 poimirlem15 36551 ismtyval 36716 ismrer1 36754 lautset 39001 pautsetN 39017 hvmap1o2 40684 pwfi2f1o 41886 imasgim 41890 alephiso2 42357 f1ocof1ob2 45838 isomushgr 46542 uspgrsprfo 46574