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 6547	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6547	. 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 6537 –onto→wfo 6538 –1-1-onto→wf1o 6539

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 2156 ax-ext 2737

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-cleq 2757 df-ss 3923 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547

This theorem is used by: f1oeq23 6815 f1oeq123d 6818 f1oeq3d 6821 f1ores 6839 resin 6847 isoeq5 7328 breng 8958 xpcomf1o 9061 isinf 9232 cnfcom2 9678 fin1a2lem6 10404 pwfseqlem5 10667 pwfseq 10668 hashgf1o 14029 axdc4uzlem 14041 sumeq1 15768 prodeq1f 15987 prodeq1 15988 prodeq1i 15997 unbenlem 16994 4sqlem11 17041 gsumvalx 18770 cayley 19532 cayleyth 19533 ovolicc2lem4 25734 logf1o2 26870 uspgrf1oedg 29585 uspgredgiedg 29587 wlkiswwlks2lem4 30292 clwwlknonclwlknonf1o 30788 dlwwlknondlwlknonf1o 30791 adjbd1o 32512 rinvf1o 33050 cshf1o 33350 eulerpartgbij 34831 eulerpartlemgh 34837 derangval 35700 subfacp1lem2a 35713 subfacp1lem3 35715 subfacp1lem5 35717 mrsubff1o 36048 msubff1o 36090 cbvprodvw2 36820 bj-finsumval0 37990 f1omptsnlem 38043 f1omptsn 38044 poimirlem9 38341 poimirlem15 38347 ismtyval 38513 ismrer1 38551 lautset 40918 pautsetN 40934 hvmap1o2 42601 pwfi2f1o 43900 imasgim 43904 alephiso2 44361 f1ocof1ob2 47896 isuspgrim0lem 48735 gricushgr 48759 grtriprop 48783 grtrif1o 48784 isgrtri 48785 uspgrsprfo 48990