Theorem dfrex2 3204

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

Syntax hints:  ¬ wn 3   ↔ wb 198  ∀wral 3117  ∃wrex 3118

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  rexanali  3206  nfrexd  3214  rexim  3216  r19.23v  3232  r19.30  3292  r19.35  3294  cbvrexf  3378  rspcimedv  3528  sbcrext  3736  cbvrexcsf  3790  rabn0  4187  r19.9rzv  4287  rexxfrd  5109  rexxfr2d  5111  rexxfrd2  5113  rexxfr  5116  rexiunxp  5495  rexxpf  5502  rexrnmpt  6618  cbvexfo  6800  rexrnmpt2  7036  tz7.49  7806  dfsup2  8619  supnub  8637  infnlb  8667  wofib  8719  zfregs2  8886  alephval3  9246  ac6n  9622  prmreclem5  15995  sylow1lem3  18366  ordtrest2lem  21378  trfil2  22061  alexsubALTlem3  22223  alexsubALTlem4  22224  evth  23128  lhop1lem  24175  vdn0conngrumgrv2  27561  nmobndseqi  28178  chpssati  29766  chrelat3  29774  nn0min  30103  xrnarchi  30272  ordtrest2NEWlem  30502  dffr5  32174  nosupbnd1lem4  32385  poimirlem1  33947  poimirlem26  33972  poimirlem27  33973  fdc  34076  lpssat  35081  lssat  35084  lfl1  35138  atlrelat1  35389  unxpwdom3  38501  ss2iundf  38785  zfregs2VD  39888