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 6838

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 6801	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6818	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6568	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6568	. 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 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560

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 2007 ax-9 2118 ax-ext 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568

This theorem is referenced by: f1oeq23 6839 f1oeq123d 6842 f1oeq3d 6845 f1ores 6862 resin 6870 isoeq5 7341 breng 8994 xpcomf1o 9101 isinf 9296 isinfOLD 9297 cnfcom2 9742 fin1a2lem6 10445 pwfseqlem5 10703 pwfseq 10704 hashgf1o 14012 axdc4uzlem 14024 sumeq1 15725 prodeq1f 15942 prodeq1 15943 prodeq1i 15952 unbenlem 16946 4sqlem11 16993 gsumvalx 18689 cayley 19432 cayleyth 19433 ovolicc2lem4 25555 logf1o2 26692 uspgrf1oedg 29190 uspgredgiedg 29192 wlkiswwlks2lem4 29892 clwwlknonclwlknonf1o 30381 dlwwlknondlwlknonf1o 30384 adjbd1o 32104 rinvf1o 32640 cshf1o 32947 eulerpartgbij 34374 eulerpartlemgh 34380 derangval 35172 subfacp1lem2a 35185 subfacp1lem3 35187 subfacp1lem5 35189 mrsubff1o 35520 msubff1o 35562 cbvprodvw2 36248 bj-finsumval0 37286 f1omptsnlem 37337 f1omptsn 37338 poimirlem9 37636 poimirlem15 37642 ismtyval 37807 ismrer1 37845 lautset 40084 pautsetN 40100 hvmap1o2 41767 pwfi2f1o 43108 imasgim 43112 alephiso2 43571 f1ocof1ob2 47094 isuspgrim0lem 47871 gricushgr 47886 grtriprop 47908 grtrif1o 47909 isgrtri 47910 uspgrsprfo 48064