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 6757

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 6718	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6737	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6486	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6486	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 –1-1→wf1 6476 –onto→wfo 6477 –1-1-onto→wf1o 6478

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2707

This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3443 df-in 3905 df-ss 3915 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486

This theorem is referenced by: f1oeq23 6758 f1oeq123d 6761 f1oeq3d 6764 f1ores 6781 resin 6789 isoeq5 7248 breng 8813 brenOLD 8815 xpcomf1o 8926 isinf 9125 isinfOLD 9126 cnfcom2 9559 fin1a2lem6 10262 pwfseqlem5 10520 pwfseq 10521 hashgf1o 13792 axdc4uzlem 13804 sumeq1 15499 prodeq1f 15717 unbenlem 16706 4sqlem11 16753 gsumvalx 18457 cayley 19118 cayleyth 19119 ovolicc2lem4 24790 logf1o2 25911 uspgrf1oedg 27832 wlkiswwlks2lem4 28525 clwwlknonclwlknonf1o 29014 dlwwlknondlwlknonf1o 29017 adjbd1o 30735 rinvf1o 31252 cshf1o 31521 eulerpartgbij 32639 eulerpartlemgh 32645 derangval 33428 subfacp1lem2a 33441 subfacp1lem3 33443 subfacp1lem5 33445 mrsubff1o 33776 msubff1o 33818 bj-finsumval0 35561 f1omptsnlem 35612 f1omptsn 35613 poimirlem9 35891 poimirlem15 35897 ismtyval 36063 ismrer1 36101 lautset 38350 pautsetN 38366 hvmap1o2 40033 pwfi2f1o 41184 imasgim 41188 alephiso2 41487 f1ocof1ob2 44925 isomushgr 45629 uspgrsprfo 45661