Theorem dfrex2 3095

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

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

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 3083  df-rex 3093

This theorem is used by:  rexanali  3122  r19.23v  3195  nfrexdw  3314  cbvrexf  3353  nfrexd  3365  rspcimedv  3575  rexab  3661  sbcrext  3829  cbvrexcsf  3899  rabn0  4349  rexn0  4462  r19.9rzv  4471  rexsng  4647  rexxfrd  5385  rexxfr2d  5387  rexxfrd2  5389  rexxfr  5392  rexiunxp  5831  rexxpf  5838  rexrnmptw  7097  rexrnmpt  7099  rexima  7243  cbvexfo  7299  rexrnmpo  7563  tz7.49  8441  dfsup2  9414  supnub  9432  infnlb  9463  wofib  9517  zfregs2  9712  alephval3  10113  ac6n  10487  prmreclem5  17005  sylow1lem3  19701  ordtrest2lem  23397  trfil2  24081  alexsubALTlem3  24243  alexsubALTlem4  24244  evth  25155  lhop1lem  26209  nosupbnd1lem4  27912  vdn0conngrumgrv2  30584  nmobndseqi  31168  chpssati  32752  chrelat3  32760  nn0min  33202  xrnarchi  33535  0nellinds  33716  ordtrest2NEWlem  34343  dffr5  36267  poimirlem1  38313  poimirlem26  38338  poimirlem27  38339  fdc  38437  lpssat  39828  lssat  39831  lfl1  39885  atlrelat1  40136  unxpwdom3  43863  onsupeqnmax  44015  sucomisnotcard  44311  ss2iundf  44426  zfregs2VD  45590  rext0  45688