Theorem dfrex2 3065

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3052  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  rexanali  3092  r19.23v  3165  nfrexdw  3284  cbvrexf  3333  nfrexd  3345  rspcimedv  3569  rexab  3655  sbcrext  3825  cbvrexcsf  3894  rabn0  4343  rexn0  4451  r19.9rzv  4460  rexsng  4635  rexxfrd  5356  rexxfr2d  5358  rexxfrd2  5360  rexxfr  5363  rexiunxp  5797  rexxpf  5804  rexrnmptw  7049  rexrnmpt  7051  rexima  7194  cbvexfo  7246  rexrnmpo  7508  tz7.49  8386  dfsup2  9359  supnub  9377  infnlb  9408  wofib  9462  zfregs2  9654  alephval3  10032  ac6n  10407  prmreclem5  16860  sylow1lem3  19541  ordtrest2lem  23159  trfil2  23843  alexsubALTlem3  24005  alexsubALTlem4  24006  evth  24926  lhop1lem  25986  nosupbnd1lem4  27691  vdn0conngrumgrv2  30283  nmobndseqi  30866  chpssati  32450  chrelat3  32458  nn0min  32911  xrnarchi  33277  0nellinds  33462  ordtrest2NEWlem  34099  dffr5  35967  poimirlem1  37866  poimirlem26  37891  poimirlem27  37892  fdc  37990  lpssat  39383  lssat  39386  lfl1  39440  atlrelat1  39691  unxpwdom3  43446  onsupeqnmax  43598  sucomisnotcard  43894  ss2iundf  44009  zfregs2VD  45190  rext0  45288