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.) (Proof shortened by AV, 7-Apr-2023.) |
Ref | Expression |
---|---|
ralsng.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexsng | ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1911 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ralsng.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rexsngf 4604 | 1 ⊢ (𝐴 ∈ 𝑉 → (∃𝑥 ∈ {𝐴}𝜑 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ∈ wcel 2110 ∃wrex 3139 {csn 4561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-v 3497 df-sbc 3773 df-sn 4562 |
This theorem is referenced by: rexsn 4614 rextpg 4629 iunxsng 5005 frirr 5527 frsn 5634 imasng 5946 scshwfzeqfzo 14182 dvdsprmpweqnn 16215 mnd1 17946 grp1 18200 elntg2 26765 1loopgrvd0 27280 1egrvtxdg0 27287 nfrgr2v 28045 1vwmgr 28049 elgrplsmsn 30939 ballotlemfc0 31745 ballotlemfcc 31746 bj-restsn 34367 elpaddat 36934 elpadd2at 36936 brfvidRP 40026 mnuunid 40606 iccelpart 43586 zlidlring 44192 lco0 44475 |
Copyright terms: Public domain | W3C validator |