![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexsng | Structured version Visualization version Unicode 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 4004 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ralsng.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | sbcieg 3300 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl5bb 261 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-rex 2743 df-v 3047 df-sbc 3268 df-sn 3969 |
This theorem is referenced by: rexsn 4011 rexprg 4022 rextpg 4024 iunxsng 4360 frirr 4811 frsn 4905 imasng 5190 scshwfzeqfzo 12925 mnd1 16577 mnd1OLD 16578 grp1 16758 frgra2v 25727 1vwmgra 25731 ballotlemfc0 29325 ballotlemfcc 29326 elpaddat 33369 elpadd2at 33371 brfvidRP 36280 iccelpart 38747 zlidlring 39981 lco0 40273 |
Copyright terms: Public domain | W3C validator |