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 6811

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 6772	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6791	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 643	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6544	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6544	. 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

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-9 2159 ax-ext 2741

This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1807 df-cleq 2761 df-ss 3930 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544

This theorem is referenced by: f1oeq23 6812 f1oeq123d 6815 f1oeq3d 6818 f1ores 6836 resin 6844 isoeq5 7320 breng 8952 xpcomf1o 9054 isinf 9225 cnfcom2 9671 fin1a2lem6 10389 pwfseqlem5 10648 pwfseq 10649 hashgf1o 14007 axdc4uzlem 14019 sumeq1 15740 prodeq1f 15960 prodeq1 15961 prodeq1i 15970 unbenlem 16968 4sqlem11 17015 gsumvalx 18734 cayley 19484 cayleyth 19485 ovolicc2lem4 25648 logf1o2 26781 uspgrf1oedg 29464 uspgredgiedg 29466 wlkiswwlks2lem4 30162 clwwlknonclwlknonf1o 30654 dlwwlknondlwlknonf1o 30657 adjbd1o 32378 rinvf1o 32916 cshf1o 33223 eulerpartgbij 34707 eulerpartlemgh 34713 derangval 35592 subfacp1lem2a 35605 subfacp1lem3 35607 subfacp1lem5 35609 mrsubff1o 35940 msubff1o 35982 cbvprodvw2 36682 bj-finsumval0 37851 f1omptsnlem 37904 f1omptsn 37905 poimirlem9 38202 poimirlem15 38208 ismtyval 38373 ismrer1 38411 lautset 40780 pautsetN 40796 hvmap1o2 42463 pwfi2f1o 43749 imasgim 43753 alephiso2 44210 f1ocof1ob2 47742 isuspgrim0lem 48581 gricushgr 48605 grtriprop 48629 grtrif1o 48630 isgrtri 48631 uspgrsprfo 48836