Theorem dfrex2 3089

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 3088	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
2	1	con2bii 360	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  rexanali  3116  r19.23v  3189  nfrexdw  3308  cbvrexf  3346  nfrexd  3358  rspcimedv  3567  rexab  3652  sbcrext  3819  cbvrexcsf  3889  rabn0  4338  rexn0  4451  r19.9rzv  4460  rexsng  4633  rexxfrd  5370  rexxfr2d  5372  rexxfrd2  5374  rexxfr  5377  rexiunxp  5816  rexxpf  5824  rexrnmptw  7095  rexrnmpt  7097  rexima  7244  cbvexfo  7298  rexrnmpo  7560  tz7.49  8458  dfsup2  9439  supnub  9457  infnlb  9488  wofib  9542  zfregs2  9737  alephval3  10192  ac6n  10566  prmreclem5  17103  sylow1lem3  19819  ordtrest2lem  23526  trfil2  24211  alexsubALTlem3  24373  alexsubALTlem4  24374  evth  25285  lhop1lem  26338  nosupbnd1lem4  28073  vdn0conngrumgrv2  30802  nmobndseqi  31386  chpssati  32970  chrelat3  32978  nn0min  33458  xrnarchi  33791  0nellinds  33972  ordtrest2NEWlem  34600  onprcf1acwevd  35966  prconf1acwevd  35967  dffr5  36611  poimirlem1  38632  poimirlem26  38657  poimirlem27  38658  fdc  38772  lpssat  40163  lssat  40166  lfl1  40220  atlrelat1  40471  unxpwdom3  44190  onsupeqnmax  44342  sucomisnotcard  44638  ss2iundf  44752  zfregs2VD  45916  rext0  46014