Theorem dfrex2 3091

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wral 3078  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3079  df-rex 3089

This theorem is used by:  rexanali  3118  r19.23v  3191  nfrexdw  3310  cbvrexf  3348  nfrexd  3360  rspcimedv  3570  rexab  3656  sbcrext  3823  cbvrexcsf  3893  rabn0  4342  rexn0  4455  r19.9rzv  4464  rexsng  4640  rexxfrd  5378  rexxfr2d  5380  rexxfrd2  5382  rexxfr  5385  rexiunxp  5824  rexxpf  5831  rexrnmptw  7092  rexrnmpt  7094  rexima  7241  cbvexfo  7295  rexrnmpo  7557  tz7.49  8438  dfsup2  9418  supnub  9436  infnlb  9467  wofib  9521  zfregs2  9716  alephval3  10117  ac6n  10491  prmreclem5  17018  sylow1lem3  19733  ordtrest2lem  23434  trfil2  24119  alexsubALTlem3  24281  alexsubALTlem4  24282  evth  25193  lhop1lem  26247  nosupbnd1lem4  27955  vdn0conngrumgrv2  30684  nmobndseqi  31268  chpssati  32852  chrelat3  32860  nn0min  33299  xrnarchi  33632  0nellinds  33813  ordtrest2NEWlem  34440  dffr5  36341  poimirlem1  38378  poimirlem26  38403  poimirlem27  38404  fdc  38503  lpssat  39894  lssat  39897  lfl1  39951  atlrelat1  40202  unxpwdom3  43944  onsupeqnmax  44096  sucomisnotcard  44392  ss2iundf  44507  zfregs2VD  45671  rext0  45769