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 6798

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 6759	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6778	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 641	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6530	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6530	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1562 –1-1→wf1 6520 –onto→wfo 6521 –1-1-onto→wf1o 6522

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-9 2154 ax-ext 2736

This theorem depends on definitions: df-bi 209 df-an 400 df-ex 1802 df-cleq 2756 df-ss 3923 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530

This theorem is referenced by: f1oeq23 6799 f1oeq123d 6802 f1oeq3d 6805 f1ores 6823 resin 6831 isoeq5 7307 breng 8938 xpcomf1o 9040 isinf 9211 cnfcom2 9659 fin1a2lem6 10364 pwfseqlem5 10623 pwfseq 10624 hashgf1o 13986 axdc4uzlem 13998 sumeq1 15718 prodeq1f 15938 prodeq1 15939 prodeq1i 15948 unbenlem 16946 4sqlem11 16993 gsumvalx 18712 cayley 19456 cayleyth 19457 ovolicc2lem4 25584 logf1o2 26717 uspgrf1oedg 29376 uspgredgiedg 29378 wlkiswwlks2lem4 30074 clwwlknonclwlknonf1o 30566 dlwwlknondlwlknonf1o 30569 adjbd1o 32290 rinvf1o 32834 cshf1o 33142 eulerpartgbij 34671 eulerpartlemgh 34677 derangval 35522 subfacp1lem2a 35535 subfacp1lem3 35537 subfacp1lem5 35539 mrsubff1o 35870 msubff1o 35912 cbvprodvw2 36612 bj-finsumval0 37782 f1omptsnlem 37835 f1omptsn 37836 poimirlem9 38133 poimirlem15 38139 ismtyval 38304 ismrer1 38342 lautset 40711 pautsetN 40727 hvmap1o2 42394 pwfi2f1o 43678 imasgim 43682 alephiso2 44139 f1ocof1ob2 47681 isuspgrim0lem 48520 gricushgr 48544 grtriprop 48568 grtrif1o 48569 isgrtri 48570 uspgrsprfo 48775