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 6852

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 6814	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6832	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 631	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6580	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6580	. 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 1537 –1-1→wf1 6570 –onto→wfo 6571 –1-1-onto→wf1o 6572

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2711

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1778 df-cleq 2732 df-ss 3993 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580

This theorem is referenced by: f1oeq23 6853 f1oeq123d 6856 f1oeq3d 6859 f1ores 6876 resin 6884 isoeq5 7357 breng 9012 brenOLD 9014 xpcomf1o 9127 isinf 9323 isinfOLD 9324 cnfcom2 9771 fin1a2lem6 10474 pwfseqlem5 10732 pwfseq 10733 hashgf1o 14022 axdc4uzlem 14034 sumeq1 15737 prodeq1f 15954 prodeq1 15955 prodeq1i 15964 unbenlem 16955 4sqlem11 17002 gsumvalx 18714 cayley 19456 cayleyth 19457 ovolicc2lem4 25574 logf1o2 26710 uspgrf1oedg 29208 uspgredgiedg 29210 wlkiswwlks2lem4 29905 clwwlknonclwlknonf1o 30394 dlwwlknondlwlknonf1o 30397 adjbd1o 32117 rinvf1o 32649 cshf1o 32929 eulerpartgbij 34337 eulerpartlemgh 34343 derangval 35135 subfacp1lem2a 35148 subfacp1lem3 35150 subfacp1lem5 35152 mrsubff1o 35483 msubff1o 35525 cbvprodvw2 36213 bj-finsumval0 37251 f1omptsnlem 37302 f1omptsn 37303 poimirlem9 37589 poimirlem15 37595 ismtyval 37760 ismrer1 37798 lautset 40039 pautsetN 40055 hvmap1o2 41722 pwfi2f1o 43053 imasgim 43057 alephiso2 43520 f1ocof1ob2 46997 isuspgrim0lem 47755 gricushgr 47770 grtriprop 47792 grtrif1o 47793 isgrtri 47794 uspgrsprfo 47871