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 6814

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 6775	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6794	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 644	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6545	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6545	. 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 6535 –onto→wfo 6536 –1-1-onto→wf1o 6537

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 2733

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-cleq 2753 df-ss 3916 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545

This theorem is used by: f1oeq23 6815 f1oeq123d 6818 f1oeq3d 6821 f1ores 6839 resin 6847 isoeq5 7329 breng 8982 xpcomf1o 9085 isinf 9256 cnfcom2 9703 fin1a2lem6 10483 pwfseqlem5 10748 pwfseq 10749 hashgf1o 14114 axdc4uzlem 14126 sumeq1 15856 prodeq1f 16075 prodeq1 16076 prodeq1i 16085 unbenlem 17086 4sqlem11 17133 gsumvalx 18865 cayley 19628 cayleyth 19629 ovolicc2lem4 25841 logf1o2 26978 uspgrf1oedg 29754 uspgredgiedg 29756 wlkiswwlks2lem4 30461 clwwlknonclwlknonf1o 30963 dlwwlknondlwlknonf1o 30966 adjbd1o 32687 rinvf1o 33224 cshf1o 33523 eulerpartgbij 35004 eulerpartlemgh 35010 derangval 35932 subfacp1lem2a 35945 subfacp1lem3 35947 subfacp1lem5 35949 mrsubff1o 36280 msubff1o 36322 cbvprodvw2 37036 bj-finsumval0 38206 f1omptsnlem 38259 f1omptsn 38260 poimirlem9 38547 poimirlem15 38553 ismtyval 38734 ismrer1 38772 lautset 41139 pautsetN 41155 hvmap1o2 42822 pwfi2f1o 44097 imasgim 44101 alephiso2 44558 f1ocof1ob2 48151 isuspgrim0lem 48990 gricushgr 49014 grtriprop 49038 grtrif1o 49039 isgrtri 49040 uspgrsprfo 49245