Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-ex | Structured version Visualization version GIF 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 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wex 1695 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1473 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 195 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1697 eximal 1698 2nalexn 1745 2exnaln 1746 19.43OLD 1800 speimfw 1863 speimfwALT 1864 spimfw 1865 ax6ev 1877 cbvexvw 1957 hbe1w 1963 hbe1 2008 hbe1a 2009 axc16nf 2122 hbntOLD 2130 hbexOLD 2138 nfex 2140 nfexd 2153 cbvexv1 2164 ax6 2239 cbvex 2260 cbvexv 2263 cbvexd 2266 drex1 2315 nfexd2 2320 sbex 2451 eujustALT 2461 spcimegf 3260 spcegf 3262 spcimedv 3265 neq0f 3885 n0fOLD 3887 dfnf5 3906 ax6vsep 4713 axnulALT 4715 axpownd 9302 gchi 9325 ballotlem2 29877 axextprim 30832 axrepprim 30833 axunprim 30834 axpowprim 30835 axinfprim 30837 axacprim 30838 distel 30953 bj-axtd 31751 bj-nalnaleximiOLD 31798 bj-modald 31848 bj-modalbe 31865 bj-hbext 31888 bj-cbvexdv 31923 bj-drex1v 31937 wl-nf-nf2 32463 n0el 33164 gneispace 37452 pm10.252 37582 hbexgVD 38164 elsetrecslem 42243 |
Copyright terms: Public domain | W3C validator |