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 6765

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 6728	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6745	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6500	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6500	. 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 1542 –1-1→wf1 6490 –onto→wfo 6491 –1-1-onto→wf1o 6492

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 1912 ax-6 1969 ax-7 2010 ax-9 2124 ax-ext 2709

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1782 df-cleq 2729 df-ss 3919 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500

This theorem is referenced by: f1oeq23 6766 f1oeq123d 6769 f1oeq3d 6772 f1ores 6789 resin 6797 isoeq5 7269 breng 8896 xpcomf1o 8998 isinf 9169 cnfcom2 9615 fin1a2lem6 10319 pwfseqlem5 10578 pwfseq 10579 hashgf1o 13898 axdc4uzlem 13910 sumeq1 15616 prodeq1f 15833 prodeq1 15834 prodeq1i 15843 unbenlem 16840 4sqlem11 16887 gsumvalx 18605 cayley 19347 cayleyth 19348 ovolicc2lem4 25481 logf1o2 26619 uspgrf1oedg 29250 uspgredgiedg 29252 wlkiswwlks2lem4 29949 clwwlknonclwlknonf1o 30441 dlwwlknondlwlknonf1o 30444 adjbd1o 32164 rinvf1o 32711 cshf1o 33046 eulerpartgbij 34531 eulerpartlemgh 34537 derangval 35363 subfacp1lem2a 35376 subfacp1lem3 35378 subfacp1lem5 35380 mrsubff1o 35711 msubff1o 35753 cbvprodvw2 36443 bj-finsumval0 37492 f1omptsnlem 37543 f1omptsn 37544 poimirlem9 37832 poimirlem15 37838 ismtyval 38003 ismrer1 38041 lautset 40410 pautsetN 40426 hvmap1o2 42093 pwfi2f1o 43405 imasgim 43409 alephiso2 43866 f1ocof1ob2 47395 isuspgrim0lem 48206 gricushgr 48230 grtriprop 48254 grtrif1o 48255 isgrtri 48256 uspgrsprfo 48461