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 6807

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 6770	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6787	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6537	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6537	. 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 6527 –onto→wfo 6528 –1-1-onto→wf1o 6529

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 2707

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2727 df-ss 3943 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537

This theorem is referenced by: f1oeq23 6808 f1oeq123d 6811 f1oeq3d 6814 f1ores 6831 resin 6839 isoeq5 7313 breng 8966 xpcomf1o 9073 isinf 9266 isinfOLD 9267 cnfcom2 9714 fin1a2lem6 10417 pwfseqlem5 10675 pwfseq 10676 hashgf1o 13987 axdc4uzlem 13999 sumeq1 15703 prodeq1f 15920 prodeq1 15921 prodeq1i 15930 unbenlem 16926 4sqlem11 16973 gsumvalx 18652 cayley 19393 cayleyth 19394 ovolicc2lem4 25471 logf1o2 26609 uspgrf1oedg 29098 uspgredgiedg 29100 wlkiswwlks2lem4 29800 clwwlknonclwlknonf1o 30289 dlwwlknondlwlknonf1o 30292 adjbd1o 32012 rinvf1o 32554 cshf1o 32884 eulerpartgbij 34350 eulerpartlemgh 34356 derangval 35135 subfacp1lem2a 35148 subfacp1lem3 35150 subfacp1lem5 35152 mrsubff1o 35483 msubff1o 35525 cbvprodvw2 36211 bj-finsumval0 37249 f1omptsnlem 37300 f1omptsn 37301 poimirlem9 37599 poimirlem15 37605 ismtyval 37770 ismrer1 37808 lautset 40047 pautsetN 40063 hvmap1o2 41730 pwfi2f1o 43067 imasgim 43071 alephiso2 43529 f1ocof1ob2 47059 isuspgrim0lem 47854 gricushgr 47878 grtriprop 47901 grtrif1o 47902 isgrtri 47903 uspgrsprfo 48071