Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > foeq3 | Structured version Visualization version GIF version |
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
foeq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2833 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 630 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) |
3 | df-fo 6361 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
4 | df-fo 6361 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ran crn 5556 Fn wfn 6350 –onto→wfo 6353 |
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 1970 ax-7 2015 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-fo 6361 |
This theorem is referenced by: fimadmfo 6599 f1oeq3 6606 foeq123d 6609 resdif 6635 ncanth 7112 ffoss 7647 rneqdmfinf1o 8800 fidomdm 8801 fifo 8896 brwdom 9031 brwdom2 9037 canthwdom 9043 ixpiunwdom 9055 fin1a2lem7 9828 dmct 9946 znnen 15565 quslem 16816 znzrhfo 20694 rncmp 22004 connima 22033 conncn 22034 qtopcmplem 22315 qtoprest 22325 eupths 27979 pjhfo 29483 cycpmconjvlem 30783 msrfo 32793 ivthALT 33683 bj-inftyexpitaufo 34487 poimirlem26 34933 poimirlem27 34934 opidon2OLD 35147 founiiun0 41471 fundcmpsurinj 43589 fundcmpsurbijinj 43590 |
Copyright terms: Public domain | W3C validator |