![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexsng | Structured version Visualization version GIF version |
Description: Restricted existential quantification over a singleton. (Contributed by NM, 29-Jan-2012.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexsng | ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexsns 4408 | . 2 ⊢ (∃𝑥 ∈ {𝐴}𝜑 ↔ [𝐴 / 𝑥]𝜑) | |
2 | ralsng.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbcieg 3666 | . 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜓)) |
4 | 1, 3 | syl5bb 275 | 1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1653 ∈ wcel 2157 ∃wrex 3090 [wsbc 3633 {csn 4368 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-rex 3095 df-v 3387 df-sbc 3634 df-sn 4369 |
This theorem is referenced by: rexsn 4414 rexprg 4425 rextpg 4427 iunxsng 4792 frirr 5289 frsn 5394 imasng 5704 scshwfzeqfzo 13911 dvdsprmpweqnn 15922 mnd1 17646 grp1 17838 1loopgrvd0 26754 1egrvtxdg0 26761 nfrgr2v 27621 1vwmgr 27625 ballotlemfc0 31071 ballotlemfcc 31072 bj-restsn 33528 elpaddat 35825 elpadd2at 35827 brfvidRP 38763 iccelpart 42209 zlidlring 42727 lco0 43015 |
Copyright terms: Public domain | W3C validator |