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 6608

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 6574	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6590	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6364	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6364	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 –1-1→wf1 6354 –onto→wfo 6355 –1-1-onto→wf1o 6356

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-in 3945 df-ss 3954 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364

This theorem is referenced by: f1oeq23 6609 f1oeq123d 6612 f1oeq3d 6614 f1ores 6631 resin 6638 isoeq5 7076 bren 8520 xpcomf1o 8608 isinf 8733 cnfcom2 9167 fin1a2lem6 9829 pwfseqlem5 10087 pwfseq 10088 hashgf1o 13342 axdc4uzlem 13354 sumeq1 15047 prodeq1f 15264 unbenlem 16246 4sqlem11 16293 gsumvalx 17888 cayley 18544 cayleyth 18545 ovolicc2lem4 24123 logf1o2 25235 uspgrf1oedg 26960 wlkiswwlks2lem4 27652 clwwlknonclwlknonf1o 28143 dlwwlknondlwlknonf1o 28146 adjbd1o 29864 rinvf1o 30377 cshf1o 30638 eulerpartgbij 31632 eulerpartlemgh 31638 derangval 32416 subfacp1lem2a 32429 subfacp1lem3 32431 subfacp1lem5 32433 mrsubff1o 32764 msubff1o 32806 bj-finsumval0 34569 f1omptsnlem 34619 f1omptsn 34620 poimirlem4 34898 poimirlem9 34903 poimirlem15 34909 ismtyval 35080 ismrer1 35118 lautset 37220 pautsetN 37236 hvmap1o2 38903 pwfi2f1o 39703 imasgim 39707 alephiso2 39924 isomushgr 43998 uspgrsprfo 44030