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 6706

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 –1-1→wf1 6430 –onto→wfo 6431 –1-1-onto→wf1o 6432

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709

This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440

This theorem is referenced by: f1oeq23 6707 f1oeq123d 6710 f1oeq3d 6713 f1ores 6730 resin 6738 isoeq5 7192 breng 8742 brenOLD 8744 xpcomf1o 8848 isinf 9036 cnfcom2 9460 fin1a2lem6 10161 pwfseqlem5 10419 pwfseq 10420 hashgf1o 13691 axdc4uzlem 13703 sumeq1 15400 prodeq1f 15618 unbenlem 16609 4sqlem11 16656 gsumvalx 18360 cayley 19022 cayleyth 19023 ovolicc2lem4 24684 logf1o2 25805 uspgrf1oedg 27543 wlkiswwlks2lem4 28237 clwwlknonclwlknonf1o 28726 dlwwlknondlwlknonf1o 28729 adjbd1o 30447 rinvf1o 30965 cshf1o 31234 eulerpartgbij 32339 eulerpartlemgh 32345 derangval 33129 subfacp1lem2a 33142 subfacp1lem3 33144 subfacp1lem5 33146 mrsubff1o 33477 msubff1o 33519 bj-finsumval0 35456 f1omptsnlem 35507 f1omptsn 35508 poimirlem9 35786 poimirlem15 35792 ismtyval 35958 ismrer1 35996 lautset 38096 pautsetN 38112 hvmap1o2 39779 pwfi2f1o 40921 imasgim 40925 alephiso2 41165 f1ocof1ob2 44574 isomushgr 45278 uspgrsprfo 45310