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 6770

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 6733	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6750	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6505	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6505	. 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 6495 –onto→wfo 6496 –1-1-onto→wf1o 6497

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 2708

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1782 df-cleq 2728 df-ss 3906 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505

This theorem is referenced by: f1oeq23 6771 f1oeq123d 6774 f1oeq3d 6777 f1ores 6794 resin 6802 isoeq5 7276 breng 8902 xpcomf1o 9004 isinf 9175 cnfcom2 9623 fin1a2lem6 10327 pwfseqlem5 10586 pwfseq 10587 hashgf1o 13933 axdc4uzlem 13945 sumeq1 15651 prodeq1f 15871 prodeq1 15872 prodeq1i 15881 unbenlem 16879 4sqlem11 16926 gsumvalx 18644 cayley 19389 cayleyth 19390 ovolicc2lem4 25487 logf1o2 26614 uspgrf1oedg 29242 uspgredgiedg 29244 wlkiswwlks2lem4 29940 clwwlknonclwlknonf1o 30432 dlwwlknondlwlknonf1o 30435 adjbd1o 32156 rinvf1o 32703 cshf1o 33022 eulerpartgbij 34516 eulerpartlemgh 34522 derangval 35349 subfacp1lem2a 35362 subfacp1lem3 35364 subfacp1lem5 35366 mrsubff1o 35697 msubff1o 35739 cbvprodvw2 36429 bj-finsumval0 37599 f1omptsnlem 37652 f1omptsn 37653 poimirlem9 37950 poimirlem15 37956 ismtyval 38121 ismrer1 38159 lautset 40528 pautsetN 40544 hvmap1o2 42211 pwfi2f1o 43524 imasgim 43528 alephiso2 43985 f1ocof1ob2 47530 isuspgrim0lem 48369 gricushgr 48393 grtriprop 48417 grtrif1o 48418 isgrtri 48419 uspgrsprfo 48624