| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define existential
quantification. |
| Ref | Expression |
|---|---|
| df-ex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | vx |
. . 3
| |
| 3 | 1, 2 | wex 980 |
. 2
|
| 4 | 1 | wn 2 |
. . . 4
|
| 5 | 4, 2 | wal 954 |
. . 3
|
| 6 | 5 | wn 2 |
. 2
|
| 7 | 3, 6 | wb 146 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: a6e 990 hbex 1006 hbe1 1016 19.8a 1029 alnex 1033 19.9t 1035 19.22 1039 19.35 1075 19.30 1085 19.43 1088 19.41 1095 ax9o 1122 a9e 1125 drex1 1156 a4ime 1160 cbvex 1166 equs5e 1198 a4sbe 1243 sb8e 1262 cbvexd 1321 sbex 1348 a12stdy1 1372 a12study 1378 cla4egf 1861 ne0f 2287 eq0 2294 axpownd 4953 |