![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eldmg | Structured version Visualization version GIF version |
Description: Domain membership. Theorem 4 of [Suppes] p. 59. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Ref | Expression |
---|---|
eldmg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 5147 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥𝐵𝑦 ↔ 𝐴𝐵𝑦)) | |
2 | 1 | exbidv 1917 | . 2 ⊢ (𝑥 = 𝐴 → (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦 𝐴𝐵𝑦)) |
3 | df-dm 5683 | . 2 ⊢ dom 𝐵 = {𝑥 ∣ ∃𝑦 𝑥𝐵𝑦} | |
4 | 2, 3 | elab2g 3668 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ dom 𝐵 ↔ ∃𝑦 𝐴𝐵𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∃wex 1774 ∈ wcel 2099 class class class wbr 5144 dom cdm 5673 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3421 df-v 3465 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4324 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-br 5145 df-dm 5683 |
This theorem is referenced by: eldm2g 5897 eldm 5898 breldmg 5907 releldmb 5943 funeu 6574 fneu 6660 ndmfv 6926 erref 8744 ecdmn0 8773 rlimdm 15546 rlimdmo1 15613 iscmet3lem2 25306 dvcnp2 25935 dvcnp2OLD 25936 ulmcau 26419 pserulm 26446 mulog2sum 27561 unbdqndv1 36222 eldmres 37979 eldmressnALTV 37981 eldm4 37983 eldmres2 37984 eldmcnv 38054 funressneu 46696 afveu 46800 rlimdmafv 46824 funressndmafv2rn 46870 afv2eu 46885 rlimdmafv2 46905 |
Copyright terms: Public domain | W3C validator |