Theorem dfrex2 3072

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3060  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3061  df-rex 3070

This theorem is referenced by:  rexanali  3101  rexbiOLD  3104  r19.23v  3182  nfrexdw  3309  cbvrexf  3360  nfrexd  3372  rspcimedv  3612  rexab  3699  sbcrext  3872  cbvrexcsf  3941  rabn0  4388  r19.9rzv  4499  rexn0  4510  rexsng  4675  rexxfrd  5408  rexxfr2d  5410  rexxfrd2  5412  rexxfr  5415  rexiunxp  5850  rexxpf  5857  rexrnmptw  7114  rexrnmpt  7116  rexima  7259  cbvexfo  7311  rexrnmpo  7574  tz7.49  8486  dfsup2  9485  supnub  9503  infnlb  9533  wofib  9586  zfregs2  9774  alephval3  10151  ac6n  10526  prmreclem5  16959  sylow1lem3  19619  ordtrest2lem  23212  trfil2  23896  alexsubALTlem3  24058  alexsubALTlem4  24059  evth  24992  lhop1lem  26053  nosupbnd1lem4  27757  vdn0conngrumgrv2  30216  nmobndseqi  30799  chpssati  32383  chrelat3  32391  nn0min  32823  xrnarchi  33192  0nellinds  33399  ordtrest2NEWlem  33922  dffr5  35755  poimirlem1  37629  poimirlem26  37654  poimirlem27  37655  fdc  37753  lpssat  39015  lssat  39018  lfl1  39072  atlrelat1  39323  unxpwdom3  43112  onsupeqnmax  43264  sucomisnotcard  43562  ss2iundf  43677  zfregs2VD  44866  rext0  44964