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 6758

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 6721	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6738	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 638	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6493	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6493	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 –1-1→wf1 6483 –onto→wfo 6484 –1-1-onto→wf1o 6485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-9 2129 ax-ext 2711

This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1787 df-cleq 2731 df-ss 3900 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493

This theorem is referenced by: f1oeq23 6759 f1oeq123d 6762 f1oeq3d 6765 f1ores 6782 resin 6790 isoeq5 7266 breng 8893 xpcomf1o 8995 isinf 9166 cnfcom2 9615 fin1a2lem6 10319 pwfseqlem5 10578 pwfseq 10579 hashgf1o 13925 axdc4uzlem 13937 sumeq1 15643 prodeq1f 15863 prodeq1 15864 prodeq1i 15873 unbenlem 16871 4sqlem11 16918 gsumvalx 18636 cayley 19381 cayleyth 19382 ovolicc2lem4 25506 logf1o2 26633 uspgrf1oedg 29261 uspgredgiedg 29263 wlkiswwlks2lem4 29959 clwwlknonclwlknonf1o 30451 dlwwlknondlwlknonf1o 30454 adjbd1o 32175 rinvf1o 32723 cshf1o 33042 eulerpartgbij 34565 eulerpartlemgh 34571 derangval 35404 subfacp1lem2a 35417 subfacp1lem3 35419 subfacp1lem5 35421 mrsubff1o 35752 msubff1o 35794 cbvprodvw2 36484 bj-finsumval0 37654 f1omptsnlem 37707 f1omptsn 37708 poimirlem9 38005 poimirlem15 38011 ismtyval 38176 ismrer1 38214 lautset 40583 pautsetN 40599 hvmap1o2 42266 pwfi2f1o 43550 imasgim 43554 alephiso2 44011 f1ocof1ob2 47553 isuspgrim0lem 48392 gricushgr 48416 grtriprop 48440 grtrif1o 48441 isgrtri 48442 uspgrsprfo 48647