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 206  ∀wral 3059  ∃wrex 3068

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

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

This theorem is referenced by:  rexanali  3100  rexbiOLD  3103  r19.23v  3181  nfrexdw  3308  cbvrexf  3359  nfrexd  3371  rspcimedv  3613  rexab  3703  sbcrext  3882  cbvrexcsf  3954  rabn0  4395  r19.9rzv  4506  rexn0  4517  rexsng  4681  rexxfrd  5415  rexxfr2d  5417  rexxfrd2  5419  rexxfr  5422  rexiunxp  5854  rexxpf  5861  rexrnmptw  7115  rexrnmpt  7117  rexima  7258  cbvexfo  7310  rexrnmpo  7573  tz7.49  8484  dfsup2  9482  supnub  9500  infnlb  9530  wofib  9583  zfregs2  9771  alephval3  10148  ac6n  10523  prmreclem5  16954  sylow1lem3  19633  ordtrest2lem  23227  trfil2  23911  alexsubALTlem3  24073  alexsubALTlem4  24074  evth  25005  lhop1lem  26067  nosupbnd1lem4  27771  vdn0conngrumgrv2  30225  nmobndseqi  30808  chpssati  32392  chrelat3  32400  nn0min  32827  xrnarchi  33174  0nellinds  33378  ordtrest2NEWlem  33883  dffr5  35734  poimirlem1  37608  poimirlem26  37633  poimirlem27  37634  fdc  37732  lpssat  38995  lssat  38998  lfl1  39052  atlrelat1  39303  unxpwdom3  43084  onsupeqnmax  43236  sucomisnotcard  43534  ss2iundf  43649  zfregs2VD  44839