Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eldm2 | Structured version Visualization version GIF version |
Description: Membership in a domain. Theorem 4 of [Suppes] p. 59. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
eldm.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
eldm2 | ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldm.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | eldm2g 5761 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ dom 𝐵 ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∃wex 1771 ∈ wcel 2105 Vcvv 3492 〈cop 4563 dom cdm 5548 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-dm 5558 |
This theorem is referenced by: dmss 5764 opeldm 5769 dmin 5773 dmiun 5775 dmuni 5776 dm0 5783 reldm0 5791 dmrnssfld 5834 dmcoss 5835 dmcosseq 5837 dmres 5868 iss 5896 dmsnopg 6063 relssdmrn 6114 funssres 6391 dmfco 6750 fiun 7633 f1iun 7634 wfrlem12 7955 axdc3lem2 9861 fnpr2ob 16819 gsum2d2 19023 cnlnssadj 29784 prsdm 31056 eldm3 32894 dfdm5 32913 frrlem8 33027 frrlem10 33029 iss2 35482 |
Copyright terms: Public domain | W3C validator |