![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexsn | Structured version Visualization version GIF version |
Description: Convert an existential quantification restricted to a singleton to a substitution. (Contributed by Jeff Madsen, 5-Jan-2011.) |
Ref | Expression |
---|---|
ralsn.1 | ⊢ 𝐴 ∈ V |
ralsn.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexsn | ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsn.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | ralsn.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | rexsng 4674 | . 2 ⊢ (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 ∃wrex 3071 Vcvv 3475 {csn 4624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-v 3477 df-sn 4625 |
This theorem is referenced by: elsnres 6016 oarec 8550 snec 8762 zornn0g 10487 fpwwe2lem12 10624 elreal 11113 hashge2el2difr 14429 vdwlem6 16906 pmatcollpw3fi1 22259 restsn 22643 snclseqg 23589 ust0 23693 0slt1s 27297 cuteq1 27301 made0 27335 cofcutr 27378 mulsrid 27536 grplsm0l 32471 esum2dlem 33021 eulerpartlemgh 33308 eldm3 34662 poimirlem28 36421 heiborlem3 36587 tfsconcatrn 41963 |
Copyright terms: Public domain | W3C validator |