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 6748

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 6711	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6728	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6483	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6483	. 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 206 ∧ wa 395 = wceq 1540 –1-1→wf1 6473 –onto→wfo 6474 –1-1-onto→wf1o 6475

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-9 2119 ax-ext 2701

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2721 df-ss 3916 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483

This theorem is referenced by: f1oeq23 6749 f1oeq123d 6752 f1oeq3d 6755 f1ores 6772 resin 6780 isoeq5 7249 breng 8872 xpcomf1o 8973 isinf 9143 cnfcom2 9586 fin1a2lem6 10287 pwfseqlem5 10545 pwfseq 10546 hashgf1o 13866 axdc4uzlem 13878 sumeq1 15583 prodeq1f 15800 prodeq1 15801 prodeq1i 15810 unbenlem 16807 4sqlem11 16854 gsumvalx 18537 cayley 19280 cayleyth 19281 ovolicc2lem4 25402 logf1o2 26540 uspgrf1oedg 29105 uspgredgiedg 29107 wlkiswwlks2lem4 29804 clwwlknonclwlknonf1o 30293 dlwwlknondlwlknonf1o 30296 adjbd1o 32016 rinvf1o 32564 cshf1o 32899 eulerpartgbij 34353 eulerpartlemgh 34359 derangval 35157 subfacp1lem2a 35170 subfacp1lem3 35172 subfacp1lem5 35174 mrsubff1o 35505 msubff1o 35547 cbvprodvw2 36238 bj-finsumval0 37276 f1omptsnlem 37327 f1omptsn 37328 poimirlem9 37626 poimirlem15 37632 ismtyval 37797 ismrer1 37835 lautset 40078 pautsetN 40094 hvmap1o2 41761 pwfi2f1o 43086 imasgim 43090 alephiso2 43548 f1ocof1ob2 47080 isuspgrim0lem 47891 gricushgr 47915 grtriprop 47939 grtrif1o 47940 isgrtri 47941 uspgrsprfo 48146