Theorem dfrex2 3092

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-ral 3080  df-rex 3090

This theorem is referenced by:  rexanali  3119  r19.23v  3192  nfrexdw  3311  cbvrexf  3351  nfrexd  3363  rspcimedv  3575  rexab  3661  sbcrext  3829  cbvrexcsf  3898  rabn0  4346  rexn0  4453  r19.9rzv  4462  rexsng  4638  rexxfrd  5371  rexxfr2d  5373  rexxfrd2  5375  rexxfr  5378  rexiunxp  5817  rexxpf  5824  rexrnmptw  7080  rexrnmpt  7082  rexima  7226  cbvexfo  7278  rexrnmpo  7540  tz7.49  8420  dfsup2  9392  supnub  9410  infnlb  9441  wofib  9495  zfregs2  9690  alephval3  10082  ac6n  10457  prmreclem5  16970  sylow1lem3  19661  ordtrest2lem  23321  trfil2  24005  alexsubALTlem3  24167  alexsubALTlem4  24168  evth  25079  lhop1lem  26133  nosupbnd1lem4  27833  vdn0conngrumgrv2  30456  nmobndseqi  31040  chpssati  32624  chrelat3  32632  nn0min  33078  xrnarchi  33417  0nellinds  33600  ordtrest2NEWlem  34229  dffr5  36117  poimirlem1  38132  poimirlem26  38157  poimirlem27  38158  fdc  38256  lpssat  39649  lssat  39652  lfl1  39706  atlrelat1  39957  unxpwdom3  43684  onsupeqnmax  43836  sucomisnotcard  44132  ss2iundf  44247  zfregs2VD  45414  rext0  45512