![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldm | Structured version Visualization version GIF version |
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 2-Apr-2004.) |
Ref | Expression |
---|---|
eldm.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
eldm | ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldm.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | eldmg 5564 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∃wex 1823 ∈ wcel 2107 Vcvv 3398 class class class wbr 4886 dom cdm 5355 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-dm 5365 |
This theorem is referenced by: dmi 5585 dmcoss 5631 dmcosseq 5633 dminss 5801 dmsnn0 5854 dffun7 6162 dffun8 6163 fnres 6253 opabiota 6521 fndmdif 6584 dff3 6636 frxp 7568 suppvalbr 7580 reldmtpos 7642 dmtpos 7646 aceq3lem 9276 axdc2lem 9605 axdclem2 9677 fpwwe2lem12 9798 nqerf 10087 shftdm 14218 xpsfrnel2 16611 bcthlem4 23533 dchrisumlem3 25632 eulerpath 27645 fundmpss 32257 elfix 32599 fnsingle 32615 fnimage 32625 funpartlem 32638 dfrecs2 32646 dfrdg4 32647 knoppcnlem9 33074 prtlem16 35023 undmrnresiss 38867 |
Copyright terms: Public domain | W3C validator |