Theorem dfrex2 3071

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1778  df-ral 3060  df-rex 3069

This theorem is referenced by:  rexanali  3099  rexbiOLD  3102  r19.23v  3173  nfrexd  3268  nfrexdg  3269  cbvrexf  3374  rspcimedv  3554  rexab  3633  sbcrext  3808  cbvrexcsf  3880  rabn0  4322  r19.9rzv  4433  rexn0  4444  rexsng  4613  rexxfrd  5335  rexxfr2d  5337  rexxfrd2  5339  rexxfr  5342  rexiunxp  5753  rexxpf  5760  rexrnmptw  6991  rexrnmpt  6993  cbvexfo  7182  rexrnmpo  7433  tz7.49  8296  dfsup2  9231  supnub  9249  infnlb  9279  wofib  9332  zfregs2  9519  alephval3  9894  ac6n  10269  prmreclem5  16649  sylow1lem3  19233  ordtrest2lem  22382  trfil2  23066  alexsubALTlem3  23228  alexsubALTlem4  23229  evth  24150  lhop1lem  25205  vdn0conngrumgrv2  28588  nmobndseqi  29169  chpssati  30753  chrelat3  30761  nn0min  31162  xrnarchi  31466  0nellinds  31594  ordtrest2NEWlem  31900  dffr5  33749  nosupbnd1lem4  33942  poimirlem1  35806  poimirlem26  35831  poimirlem27  35832  fdc  35931  lpssat  37053  lssat  37056  lfl1  37110  atlrelat1  37361  unxpwdom3  40944  sucomisnotcard  41175  ss2iundf  41291  zfregs2VD  42485