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 356	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-ral 3060  df-rex 3069

This theorem is referenced by:  rexanali  3100  rexbiOLD  3103  r19.23v  3180  nfrexdw  3305  cbvrexf  3355  nfrexd  3367  rspcimedv  3604  rexab  3691  sbcrext  3868  cbvrexcsf  3940  rabn0  4386  r19.9rzv  4500  rexn0  4511  rexsng  4679  rexxfrd  5408  rexxfr2d  5410  rexxfrd2  5412  rexxfr  5415  rexiunxp  5841  rexxpf  5848  rexrnmptw  7097  rexrnmpt  7099  cbvexfo  7292  rexrnmpo  7552  tz7.49  8449  dfsup2  9443  supnub  9461  infnlb  9491  wofib  9544  zfregs2  9732  alephval3  10109  ac6n  10484  prmreclem5  16859  sylow1lem3  19511  ordtrest2lem  22929  trfil2  23613  alexsubALTlem3  23775  alexsubALTlem4  23776  evth  24707  lhop1lem  25764  nosupbnd1lem4  27448  vdn0conngrumgrv2  29714  nmobndseqi  30297  chpssati  31881  chrelat3  31889  nn0min  32291  xrnarchi  32598  0nellinds  32755  ordtrest2NEWlem  33198  dffr5  35026  poimirlem1  36794  poimirlem26  36819  poimirlem27  36820  fdc  36918  lpssat  38188  lssat  38191  lfl1  38245  atlrelat1  38496  unxpwdom3  42141  onsupeqnmax  42300  sucomisnotcard  42599  ss2iundf  42714  zfregs2VD  43906