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 6772

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 6735	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6752	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6506	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6506	. 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 6496 –onto→wfo 6497 –1-1-onto→wf1o 6498

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 3928 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506

This theorem is referenced by: f1oeq23 6773 f1oeq123d 6776 f1oeq3d 6779 f1ores 6796 resin 6804 isoeq5 7278 breng 8904 xpcomf1o 9007 isinf 9183 isinfOLD 9184 cnfcom2 9631 fin1a2lem6 10334 pwfseqlem5 10592 pwfseq 10593 hashgf1o 13912 axdc4uzlem 13924 sumeq1 15631 prodeq1f 15848 prodeq1 15849 prodeq1i 15858 unbenlem 16855 4sqlem11 16902 gsumvalx 18585 cayley 19328 cayleyth 19329 ovolicc2lem4 25454 logf1o2 26592 uspgrf1oedg 29153 uspgredgiedg 29155 wlkiswwlks2lem4 29852 clwwlknonclwlknonf1o 30341 dlwwlknondlwlknonf1o 30344 adjbd1o 32064 rinvf1o 32604 cshf1o 32934 eulerpartgbij 34356 eulerpartlemgh 34362 derangval 35147 subfacp1lem2a 35160 subfacp1lem3 35162 subfacp1lem5 35164 mrsubff1o 35495 msubff1o 35537 cbvprodvw2 36228 bj-finsumval0 37266 f1omptsnlem 37317 f1omptsn 37318 poimirlem9 37616 poimirlem15 37622 ismtyval 37787 ismrer1 37825 lautset 40069 pautsetN 40085 hvmap1o2 41752 pwfi2f1o 43078 imasgim 43082 alephiso2 43540 f1ocof1ob2 47076 isuspgrim0lem 47886 gricushgr 47910 grtriprop 47933 grtrif1o 47934 isgrtri 47935 uspgrsprfo 48129