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 6808

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 6769	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6788	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6540	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6540	. 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 401 = wceq 1570 –1-1→wf1 6530 –onto→wfo 6531 –1-1-onto→wf1o 6532

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-9 2155 ax-ext 2732

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-cleq 2752 df-ss 3916 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540

This theorem is used by: f1oeq23 6809 f1oeq123d 6812 f1oeq3d 6815 f1ores 6833 resin 6841 isoeq5 7323 breng 8964 xpcomf1o 9067 isinf 9238 cnfcom2 9684 fin1a2lem6 10410 pwfseqlem5 10675 pwfseq 10676 hashgf1o 14038 axdc4uzlem 14050 sumeq1 15779 prodeq1f 15998 prodeq1 15999 prodeq1i 16008 unbenlem 17003 4sqlem11 17050 gsumvalx 18781 cayley 19544 cayleyth 19545 ovolicc2lem4 25751 logf1o2 26890 uspgrf1oedg 29636 uspgredgiedg 29638 wlkiswwlks2lem4 30343 clwwlknonclwlknonf1o 30845 dlwwlknondlwlknonf1o 30848 adjbd1o 32569 rinvf1o 33106 cshf1o 33405 eulerpartgbij 34886 eulerpartlemgh 34892 derangval 35749 subfacp1lem2a 35762 subfacp1lem3 35764 subfacp1lem5 35766 mrsubff1o 36097 msubff1o 36139 cbvprodvw2 36870 bj-finsumval0 38040 f1omptsnlem 38093 f1omptsn 38094 poimirlem9 38381 poimirlem15 38387 ismtyval 38553 ismrer1 38591 lautset 40958 pautsetN 40974 hvmap1o2 42641 pwfi2f1o 43940 imasgim 43944 alephiso2 44401 f1ocof1ob2 47973 isuspgrim0lem 48812 gricushgr 48836 grtriprop 48860 grtrif1o 48861 isgrtri 48862 uspgrsprfo 49067