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 6823

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 6784	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6803	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6550	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6550	. 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 1541 –1-1→wf1 6540 –onto→wfo 6541 –1-1-onto→wf1o 6542

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

This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3955 df-ss 3965 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550

This theorem is referenced by: f1oeq23 6824 f1oeq123d 6827 f1oeq3d 6830 f1ores 6847 resin 6855 isoeq5 7320 breng 8950 brenOLD 8952 xpcomf1o 9063 isinf 9262 isinfOLD 9263 cnfcom2 9699 fin1a2lem6 10402 pwfseqlem5 10660 pwfseq 10661 hashgf1o 13940 axdc4uzlem 13952 sumeq1 15639 prodeq1f 15856 unbenlem 16845 4sqlem11 16892 gsumvalx 18601 cayley 19323 cayleyth 19324 ovolicc2lem4 25261 logf1o2 26382 uspgrf1oedg 28688 wlkiswwlks2lem4 29381 clwwlknonclwlknonf1o 29870 dlwwlknondlwlknonf1o 29873 adjbd1o 31593 rinvf1o 32109 cshf1o 32381 eulerpartgbij 33657 eulerpartlemgh 33663 derangval 34444 subfacp1lem2a 34457 subfacp1lem3 34459 subfacp1lem5 34461 mrsubff1o 34792 msubff1o 34834 bj-finsumval0 36469 f1omptsnlem 36520 f1omptsn 36521 poimirlem9 36800 poimirlem15 36806 ismtyval 36971 ismrer1 37009 lautset 39256 pautsetN 39272 hvmap1o2 40939 pwfi2f1o 42140 imasgim 42144 alephiso2 42611 f1ocof1ob2 46089 isomushgr 46793 uspgrsprfo 46825