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 6753

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 6716	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6733	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6488	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6488	. 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 1541 –1-1→wf1 6478 –onto→wfo 6479 –1-1-onto→wf1o 6480

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 1968 ax-7 2009 ax-9 2121 ax-ext 2703

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2723 df-ss 3914 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488

This theorem is referenced by: f1oeq23 6754 f1oeq123d 6757 f1oeq3d 6760 f1ores 6777 resin 6785 isoeq5 7255 breng 8878 xpcomf1o 8979 isinf 9149 cnfcom2 9592 fin1a2lem6 10296 pwfseqlem5 10554 pwfseq 10555 hashgf1o 13878 axdc4uzlem 13890 sumeq1 15596 prodeq1f 15813 prodeq1 15814 prodeq1i 15823 unbenlem 16820 4sqlem11 16867 gsumvalx 18584 cayley 19326 cayleyth 19327 ovolicc2lem4 25448 logf1o2 26586 uspgrf1oedg 29151 uspgredgiedg 29153 wlkiswwlks2lem4 29850 clwwlknonclwlknonf1o 30342 dlwwlknondlwlknonf1o 30345 adjbd1o 32065 rinvf1o 32612 cshf1o 32943 eulerpartgbij 34385 eulerpartlemgh 34391 derangval 35211 subfacp1lem2a 35224 subfacp1lem3 35226 subfacp1lem5 35228 mrsubff1o 35559 msubff1o 35601 cbvprodvw2 36291 bj-finsumval0 37329 f1omptsnlem 37380 f1omptsn 37381 poimirlem9 37679 poimirlem15 37685 ismtyval 37850 ismrer1 37888 lautset 40191 pautsetN 40207 hvmap1o2 41874 pwfi2f1o 43199 imasgim 43203 alephiso2 43661 f1ocof1ob2 47192 isuspgrim0lem 48003 gricushgr 48027 grtriprop 48051 grtrif1o 48052 isgrtri 48053 uspgrsprfo 48258