HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-ex 957
Description: Define existential quantification. E.xph means "there exists at least one set x such that ph is true." Definition of [Margaris] p. 49.
Assertion
Ref Expression
df-ex |- (E.xph <-> -. A.x -. ph)

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 wph . . 3 wff ph
2 vx . . 3 set x
31, 2wex 956 . 2 wff E.xph
41wn 2 . . . 4 wff -. ph
54, 2wal 950 . . 3 wff A.x -. ph
65wn 2 . 2 wff -. A.x -. ph
73, 6wb 146 1 wff (E.xph <-> -. A.x -. ph)
Colors of variables: wff set class
This definition is referenced by:  a6e 966  hbex 982  hbe1 990  19.8a 1005  alnex 1009  19.9t 1011  19.22 1015  19.35 1051  19.30 1061  19.43 1064  19.41 1071  ax9 1110  a9e 1112  drex1 1139  a4c 1143  cbvex 1149  equs5e 1182  sbea4 1227  sb8e 1246  cbvexd 1303  sbex 1330  a12stdy1 1349  a12study 1355  cla4egf 1836  ne0f 2258  eq0 2265  axpownd 4876
Copyright terms: Public domain