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 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  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  3653  sbcrext  3820  cbvrexcsf  3890  rabn0  4339  rexn0  4452  r19.9rzv  4461  rexsng  4637  rexxfrd  5374  rexxfr2d  5376  rexxfrd2  5378  rexxfr  5381  rexiunxp  5820  rexxpf  5827  rexrnmptw  7088  rexrnmpt  7090  rexima  7237  cbvexfo  7291  rexrnmpo  7553  tz7.49  8434  dfsup2  9414  supnub  9432  infnlb  9463  wofib  9517  zfregs2  9712  alephval3  10113  ac6n  10487  prmreclem5  17012  sylow1lem3  19727  ordtrest2lem  23428  trfil2  24113  alexsubALTlem3  24275  alexsubALTlem4  24276  evth  25187  lhop1lem  26240  nosupbnd1lem4  27947  vdn0conngrumgrv2  30676  nmobndseqi  31260  chpssati  32844  chrelat3  32852  nn0min  33291  xrnarchi  33624  0nellinds  33805  ordtrest2NEWlem  34432  dffr5  36333  poimirlem1  38370  poimirlem26  38395  poimirlem27  38396  fdc  38495  lpssat  39886  lssat  39889  lfl1  39943  atlrelat1  40194  unxpwdom3  43936  onsupeqnmax  44088  sucomisnotcard  44384  ss2iundf  44499  zfregs2VD  45663  rext0  45761