Theorem dfrex2 3093

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Wolf Lammen, 26-Nov-2019.)

Assertion

Ref	Expression
dfrex2	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  rexanali  3120  r19.23v  3193  nfrexdw  3312  cbvrexf  3350  nfrexd  3362  rspcimedv  3571  rexab  3656  sbcrext  3824  cbvrexcsf  3894  rabn0  4342  rexn0  4455  r19.9rzv  4464  rexsng  4637  rexxfrd  5375  rexxfr2d  5377  rexxfrd2  5379  rexxfr  5382  rexiunxp  5823  rexxpf  5831  rexrnmptw  7119  rexrnmpt  7121  rexima  7267  cbvexfo  7321  rexrnmpo  7584  tz7.49  8483  dfsup2  9463  supnub  9481  infnlb  9512  wofib  9566  zfregs2  9761  alephval3  10216  ac6n  10590  prmreclem5  17127  sylow1lem3  19844  ordtrest2lem  23551  trfil2  24236  alexsubALTlem3  24398  alexsubALTlem4  24399  evth  25310  lhop1lem  26363  nosupbnd1lem4  28098  vdn0conngrumgrv2  30827  nmobndseqi  31411  chpssati  32995  chrelat3  33003  nn0min  33482  xrnarchi  33815  0nellinds  33996  ordtrest2NEWlem  34624  onprcf1acwevd  36047  prconf1acwevd  36048  dffr5  36697  poimirlem1  38731  poimirlem26  38756  poimirlem27  38757  fdc  38871  lpssat  40262  lssat  40265  lfl1  40319  atlrelat1  40570  unxpwdom3  44290  onsupeqnmax  44441  sucomisnotcard  44737  ss2iundf  44851  zfregs2VD  46014  rext0  46112