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 6790

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 6753	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6770	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6518	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6518	. 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 6508 –onto→wfo 6509 –1-1-onto→wf1o 6510

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 2008 ax-9 2119 ax-ext 2701

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2721 df-ss 3931 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518

This theorem is referenced by: f1oeq23 6791 f1oeq123d 6794 f1oeq3d 6797 f1ores 6814 resin 6822 isoeq5 7296 breng 8927 xpcomf1o 9030 isinf 9207 isinfOLD 9208 cnfcom2 9655 fin1a2lem6 10358 pwfseqlem5 10616 pwfseq 10617 hashgf1o 13936 axdc4uzlem 13948 sumeq1 15655 prodeq1f 15872 prodeq1 15873 prodeq1i 15882 unbenlem 16879 4sqlem11 16926 gsumvalx 18603 cayley 19344 cayleyth 19345 ovolicc2lem4 25421 logf1o2 26559 uspgrf1oedg 29100 uspgredgiedg 29102 wlkiswwlks2lem4 29802 clwwlknonclwlknonf1o 30291 dlwwlknondlwlknonf1o 30294 adjbd1o 32014 rinvf1o 32554 cshf1o 32884 eulerpartgbij 34363 eulerpartlemgh 34369 derangval 35154 subfacp1lem2a 35167 subfacp1lem3 35169 subfacp1lem5 35171 mrsubff1o 35502 msubff1o 35544 cbvprodvw2 36235 bj-finsumval0 37273 f1omptsnlem 37324 f1omptsn 37325 poimirlem9 37623 poimirlem15 37629 ismtyval 37794 ismrer1 37832 lautset 40076 pautsetN 40092 hvmap1o2 41759 pwfi2f1o 43085 imasgim 43089 alephiso2 43547 f1ocof1ob2 47083 isuspgrim0lem 47893 gricushgr 47917 grtriprop 47940 grtrif1o 47941 isgrtri 47942 uspgrsprfo 48136