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 6793

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 6756	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6773	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6521	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6521	. 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 206 ∧ wa 395 = wceq 1540 –1-1→wf1 6511 –onto→wfo 6512 –1-1-onto→wf1o 6513

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-9 2119 ax-ext 2702

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2722 df-ss 3934 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521

This theorem is referenced by: f1oeq23 6794 f1oeq123d 6797 f1oeq3d 6800 f1ores 6817 resin 6825 isoeq5 7299 breng 8930 xpcomf1o 9035 isinf 9214 isinfOLD 9215 cnfcom2 9662 fin1a2lem6 10365 pwfseqlem5 10623 pwfseq 10624 hashgf1o 13943 axdc4uzlem 13955 sumeq1 15662 prodeq1f 15879 prodeq1 15880 prodeq1i 15889 unbenlem 16886 4sqlem11 16933 gsumvalx 18610 cayley 19351 cayleyth 19352 ovolicc2lem4 25428 logf1o2 26566 uspgrf1oedg 29107 uspgredgiedg 29109 wlkiswwlks2lem4 29809 clwwlknonclwlknonf1o 30298 dlwwlknondlwlknonf1o 30301 adjbd1o 32021 rinvf1o 32561 cshf1o 32891 eulerpartgbij 34370 eulerpartlemgh 34376 derangval 35161 subfacp1lem2a 35174 subfacp1lem3 35176 subfacp1lem5 35178 mrsubff1o 35509 msubff1o 35551 cbvprodvw2 36242 bj-finsumval0 37280 f1omptsnlem 37331 f1omptsn 37332 poimirlem9 37630 poimirlem15 37636 ismtyval 37801 ismrer1 37839 lautset 40083 pautsetN 40099 hvmap1o2 41766 pwfi2f1o 43092 imasgim 43096 alephiso2 43554 f1ocof1ob2 47087 isuspgrim0lem 47897 gricushgr 47921 grtriprop 47944 grtrif1o 47945 isgrtri 47946 uspgrsprfo 48140