| 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 4676 | . 2 ⊢ (𝐴 ∈ V → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 Vcvv 3480 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-v 3482 df-sn 4627 |
| This theorem is referenced by: elsnres 6039 oarec 8600 snec 8820 zornn0g 10545 fpwwe2lem12 10682 elreal 11171 hashge2el2difr 14520 vdwlem6 17024 pzriprnglem10 21501 pmatcollpw3fi1 22794 restsn 23178 snclseqg 24124 ust0 24228 0slt1s 27874 cuteq1 27878 made0 27912 cofcutr 27958 mulsrid 28139 n0scut 28338 zscut 28393 1p1e2s 28400 nohalf 28407 halfcut 28416 addhalfcut 28419 grplsm0l 33431 rprmdvdsprod 33562 esum2dlem 34093 eulerpartlemgh 34380 eldm3 35761 poimirlem28 37655 heiborlem3 37820 tfsconcatrn 43355 stgr1 47928 |
| Copyright terms: Public domain | W3C validator |