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 6774

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 6737	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6754	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6509	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6509	. 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 6499 –onto→wfo 6500 –1-1-onto→wf1o 6501

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 3920 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509

This theorem is referenced by: f1oeq23 6775 f1oeq123d 6778 f1oeq3d 6781 f1ores 6798 resin 6806 isoeq5 7279 breng 8906 xpcomf1o 9008 isinf 9179 cnfcom2 9625 fin1a2lem6 10329 pwfseqlem5 10588 pwfseq 10589 hashgf1o 13908 axdc4uzlem 13920 sumeq1 15626 prodeq1f 15843 prodeq1 15844 prodeq1i 15853 unbenlem 16850 4sqlem11 16897 gsumvalx 18615 cayley 19360 cayleyth 19361 ovolicc2lem4 25494 logf1o2 26632 uspgrf1oedg 29264 uspgredgiedg 29266 wlkiswwlks2lem4 29963 clwwlknonclwlknonf1o 30455 dlwwlknondlwlknonf1o 30458 adjbd1o 32179 rinvf1o 32726 cshf1o 33061 eulerpartgbij 34556 eulerpartlemgh 34562 derangval 35389 subfacp1lem2a 35402 subfacp1lem3 35404 subfacp1lem5 35406 mrsubff1o 35737 msubff1o 35779 cbvprodvw2 36469 bj-finsumval0 37567 f1omptsnlem 37618 f1omptsn 37619 poimirlem9 37909 poimirlem15 37915 ismtyval 38080 ismrer1 38118 lautset 40487 pautsetN 40503 hvmap1o2 42170 pwfi2f1o 43482 imasgim 43486 alephiso2 43943 f1ocof1ob2 47471 isuspgrim0lem 48282 gricushgr 48306 grtriprop 48330 grtrif1o 48331 isgrtri 48332 uspgrsprfo 48537