Theorem dfrex2 3161

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

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wral 3061  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  rexim  3163  rexbi  3164  rexanali  3184  r19.23v  3198  nfrexd  3226  nfrexdg  3227  cbvrexfw  3346  cbvrexf  3348  rspcimedv  3528  sbcrext  3785  cbvrexcsf  3857  rabn0  4300  r19.9rzv  4411  rexn0  4422  rexsng  4590  rexxfrd  5302  rexxfr2d  5304  rexxfrd2  5306  rexxfr  5309  rexiunxp  5709  rexxpf  5716  rexrnmptw  6914  rexrnmpt  6916  cbvexfo  7100  rexrnmpo  7349  tz7.49  8181  dfsup2  9060  supnub  9078  infnlb  9108  wofib  9161  zfregs2  9349  alephval3  9724  ac6n  10099  prmreclem5  16473  sylow1lem3  18989  ordtrest2lem  22100  trfil2  22784  alexsubALTlem3  22946  alexsubALTlem4  22947  evth  23856  lhop1lem  24910  vdn0conngrumgrv2  28279  nmobndseqi  28860  chpssati  30444  chrelat3  30452  nn0min  30854  xrnarchi  31157  0nellinds  31280  ordtrest2NEWlem  31586  dffr5  33439  nosupbnd1lem4  33651  poimirlem1  35515  poimirlem26  35540  poimirlem27  35541  fdc  35640  lpssat  36764  lssat  36767  lfl1  36821  atlrelat1  37072  unxpwdom3  40623  ss2iundf  40944  zfregs2VD  42134