![]() |
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 5351 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∃wex 1744 ∈ wcel 2030 Vcvv 3231 class class class wbr 4685 dom cdm 5143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-dm 5153 |
This theorem is referenced by: dmi 5372 dmcoss 5417 dmcosseq 5419 dminss 5582 dmsnn0 5635 dffun7 5953 dffun8 5954 fnres 6045 opabiota 6300 fndmdif 6361 dff3 6412 frxp 7332 suppvalbr 7344 reldmtpos 7405 dmtpos 7409 aceq3lem 8981 axdc2lem 9308 axdclem2 9380 fpwwe2lem12 9501 nqerf 9790 shftdm 13855 xpsfrnel2 16272 bcthlem4 23170 dchrisumlem3 25225 eulerpath 27219 fundmpss 31790 elfix 32135 fnsingle 32151 fnimage 32161 funpartlem 32174 dfrecs2 32182 dfrdg4 32183 knoppcnlem9 32616 prtlem16 34473 undmrnresiss 38227 |
Copyright terms: Public domain | W3C validator |