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 6762

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 6725	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6742	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6497	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6497	. 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 6487 –onto→wfo 6488 –1-1-onto→wf1o 6489

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 2123 ax-ext 2706

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2726 df-ss 3916 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497

This theorem is referenced by: f1oeq23 6763 f1oeq123d 6766 f1oeq3d 6769 f1ores 6786 resin 6794 isoeq5 7265 breng 8890 xpcomf1o 8992 isinf 9163 cnfcom2 9609 fin1a2lem6 10313 pwfseqlem5 10572 pwfseq 10573 hashgf1o 13892 axdc4uzlem 13904 sumeq1 15610 prodeq1f 15827 prodeq1 15828 prodeq1i 15837 unbenlem 16834 4sqlem11 16881 gsumvalx 18599 cayley 19341 cayleyth 19342 ovolicc2lem4 25475 logf1o2 26613 uspgrf1oedg 29195 uspgredgiedg 29197 wlkiswwlks2lem4 29894 clwwlknonclwlknonf1o 30386 dlwwlknondlwlknonf1o 30389 adjbd1o 32109 rinvf1o 32657 cshf1o 32993 eulerpartgbij 34478 eulerpartlemgh 34484 derangval 35310 subfacp1lem2a 35323 subfacp1lem3 35325 subfacp1lem5 35327 mrsubff1o 35658 msubff1o 35700 cbvprodvw2 36390 bj-finsumval0 37429 f1omptsnlem 37480 f1omptsn 37481 poimirlem9 37769 poimirlem15 37775 ismtyval 37940 ismrer1 37978 lautset 40281 pautsetN 40297 hvmap1o2 41964 pwfi2f1o 43280 imasgim 43284 alephiso2 43741 f1ocof1ob2 47270 isuspgrim0lem 48081 gricushgr 48105 grtriprop 48129 grtrif1o 48130 isgrtri 48131 uspgrsprfo 48336