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 6690

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 6651	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6670	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 630	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6425	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6425	. 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 395 = wceq 1539 –1-1→wf1 6415 –onto→wfo 6416 –1-1-onto→wf1o 6417

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709

This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1542 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-v 3424 df-in 3890 df-ss 3900 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425

This theorem is referenced by: f1oeq23 6691 f1oeq123d 6694 f1oeq3d 6697 f1ores 6714 resin 6721 isoeq5 7172 breng 8700 brenOLD 8702 xpcomf1o 8801 isinf 8965 cnfcom2 9390 fin1a2lem6 10092 pwfseqlem5 10350 pwfseq 10351 hashgf1o 13619 axdc4uzlem 13631 sumeq1 15328 prodeq1f 15546 unbenlem 16537 4sqlem11 16584 gsumvalx 18275 cayley 18937 cayleyth 18938 ovolicc2lem4 24589 logf1o2 25710 uspgrf1oedg 27446 wlkiswwlks2lem4 28138 clwwlknonclwlknonf1o 28627 dlwwlknondlwlknonf1o 28630 adjbd1o 30348 rinvf1o 30866 cshf1o 31136 eulerpartgbij 32239 eulerpartlemgh 32245 derangval 33029 subfacp1lem2a 33042 subfacp1lem3 33044 subfacp1lem5 33046 mrsubff1o 33377 msubff1o 33419 bj-finsumval0 35383 f1omptsnlem 35434 f1omptsn 35435 poimirlem9 35713 poimirlem15 35719 ismtyval 35885 ismrer1 35923 lautset 38023 pautsetN 38039 hvmap1o2 39706 pwfi2f1o 40837 imasgim 40841 alephiso2 41054 f1ocof1ob2 44461 isomushgr 45166 uspgrsprfo 45198