Theorem dfrex2 3088

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3075  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  rexanali  3115  r19.23v  3188  nfrexdw  3307  cbvrexf  3347  nfrexd  3359  rspcimedv  3572  rexab  3657  sbcrext  3826  cbvrexcsf  3895  rabn0  4342  rexn0  4449  r19.9rzv  4458  rexsng  4634  rexxfrd  5365  rexxfr2d  5367  rexxfrd2  5369  rexxfr  5372  rexiunxp  5810  rexxpf  5817  rexrnmptw  7072  rexrnmpt  7074  rexima  7218  cbvexfo  7270  rexrnmpo  7532  tz7.49  8411  dfsup2  9387  supnub  9405  infnlb  9436  wofib  9490  zfregs2  9685  alephval3  10063  ac6n  10439  prmreclem5  16939  sylow1lem3  19623  ordtrest2lem  23243  trfil2  23927  alexsubALTlem3  24089  alexsubALTlem4  24090  evth  25001  lhop1lem  26055  nosupbnd1lem4  27752  vdn0conngrumgrv2  30344  nmobndseqi  30928  chpssati  32512  chrelat3  32520  nn0min  32973  xrnarchi  33325  0nellinds  33517  ordtrest2NEWlem  34180  dffr5  36068  poimirlem1  38084  poimirlem26  38109  poimirlem27  38110  fdc  38208  lpssat  39601  lssat  39604  lfl1  39658  atlrelat1  39909  unxpwdom3  43636  onsupeqnmax  43788  sucomisnotcard  44084  ss2iundf  44199  zfregs2VD  45380  rext0  45478