Theorem dfrex2 3092

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  rexanali  3119  r19.23v  3192  nfrexdw  3311  cbvrexf  3350  nfrexd  3362  rspcimedv  3573  rexab  3659  sbcrext  3827  cbvrexcsf  3897  rabn0  4347  rexn0  4458  r19.9rzv  4467  rexsng  4643  rexxfrd  5382  rexxfr2d  5384  rexxfrd2  5386  rexxfr  5389  rexiunxp  5828  rexxpf  5835  rexrnmptw  7092  rexrnmpt  7094  rexima  7238  cbvexfo  7290  rexrnmpo  7552  tz7.49  8433  dfsup2  9405  supnub  9423  infnlb  9454  wofib  9508  zfregs2  9703  alephval3  10095  ac6n  10470  prmreclem5  16981  sylow1lem3  19671  ordtrest2lem  23341  trfil2  24025  alexsubALTlem3  24187  alexsubALTlem4  24188  evth  25099  lhop1lem  26153  nosupbnd1lem4  27853  vdn0conngrumgrv2  30525  nmobndseqi  31109  chpssati  32693  chrelat3  32701  nn0min  33143  xrnarchi  33482  0nellinds  33663  ordtrest2NEWlem  34290  dffr5  36224  poimirlem1  38250  poimirlem26  38275  poimirlem27  38276  fdc  38374  lpssat  39765  lssat  39768  lfl1  39822  atlrelat1  40073  unxpwdom3  43802  onsupeqnmax  43954  sucomisnotcard  44250  ss2iundf  44365  zfregs2VD  45529  rext0  45627