![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-ex | Unicode version |
Description: Define existential
quantification. ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-ex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | 1, 2 | wex 1547 |
. 2
![]() ![]() ![]() ![]() |
4 | 1 | wn 3 |
. . . 4
![]() ![]() ![]() |
5 | 4, 2 | wal 1546 |
. . 3
![]() ![]() ![]() ![]() ![]() |
6 | 5 | wn 3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wb 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: alnex 1549 2nalexn 1579 19.43OLD 1613 ax17e 1625 speimfw 1652 spimfw 1653 a9ev 1664 19.8wOLD 1701 19.9vOLD 1706 cbvexvw 1713 hbe1w 1719 hbe1 1742 excom 1752 a6e 1763 19.8aOLD 1768 hbnt 1795 19.9htOLD 1799 spimehOLD 1836 hbex 1859 nfexOLD 1862 nfexd 1869 19.9tOLD 1876 equs5eOLD 1907 ax9 1949 spimeOLD 1957 ax12olem5OLD 1981 ax10OLD 1998 a9eOLD 2000 drex1 2034 nfexd2 2040 cbvex 2060 cbvexd 2064 spsbe 2132 sbex 2186 eujustALT 2265 spcimegf 2998 spcegf 3000 spcimedv 3003 n0f 3604 eq0 3610 ax9vsep 4302 axnulALT 4304 axpownd 8440 gchi 8463 xfree2 23909 ballotlem2 24707 axextprim 25111 axrepprim 25112 axunprim 25113 axpowprim 25114 axinfprim 25116 axacprim 25117 distel 25382 n0el 26606 pm10.252 27432 pm10.56 27441 2exnaln 27448 hbexgVD 28736 hbexwAUX7 29167 nfexwAUX7 29169 nfexdwAUX7 29171 a9eNEW7 29188 ax10NEW7 29191 drex1NEW7 29212 spimeNEW7 29227 cbvexwAUX7 29236 spsbeNEW7 29287 sb8ewAUX7 29307 sbexNEW7 29330 hbexOLD7 29381 nfexOLD7 29384 nfexdOLD7 29387 nfexd2OLD7 29414 cbvexOLD7 29422 cbvexdOLD7 29431 sb8eOLD7 29453 |
Copyright terms: Public domain | W3C validator |