![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-ex | Unicode version |
Description: Define existential quantification. means "there exists at least one set such that is true." Definition of [Margaris] p. 49. (Contributed by NM, 10-Jan-1993.) |
Ref | Expression |
---|---|
df-ex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | wex 1612 | . 2 |
4 | 1 | wn 3 | . . . 4 |
5 | 4, 2 | wal 1393 | . . 3 |
6 | 5 | wn 3 | . 2 |
7 | 3, 6 | wb 184 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1614 eximal 1615 2nalexn 1649 2exnaln 1650 19.43OLD 1694 speimfw 1735 speimfwOLD 1736 spimfw 1737 ax6ev 1749 cbvexvw 1810 hbe1w 1815 hbe1 1839 excom 1849 axc7e 1862 hbnt 1894 hbex 1946 nfexd 1952 ax6 2003 cbvex 2022 cbvexd 2026 drex1 2069 nfexd2 2074 sbex 2207 eujustALT 2285 spcimegf 3188 spcegf 3190 spcimedv 3193 n0f 3793 eq0 3800 ax6vsep 4577 axnulALT 4579 axpownd 8999 gchi 9023 ballotlem2 28427 axextprim 29073 axrepprim 29074 axunprim 29075 axpowprim 29076 axinfprim 29078 axacprim 29079 distel 29236 n0el 30600 pm10.252 31266 hbexgVD 33706 bj-axtd 34182 bj-nalnaleximiOLD 34222 bj-modalbe 34241 bj-hbext 34264 bj-cbvexv 34297 bj-cbvexdv 34301 bj-drex1v 34327 |
Copyright terms: Public domain | W3C validator |