Theorem dfrex2 3067

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

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wral 3054  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  rexanali  3094  r19.23v  3167  nfrexdw  3286  cbvrexf  3326  nfrexd  3338  rspcimedv  3558  rexab  3643  sbcrext  3812  cbvrexcsf  3881  rabn0  4324  rexn0  4431  r19.9rzv  4440  rexsng  4615  rexxfrd  5345  rexxfr2d  5347  rexxfrd2  5349  rexxfr  5352  rexiunxp  5789  rexxpf  5796  rexrnmptw  7043  rexrnmpt  7045  rexima  7189  cbvexfo  7241  rexrnmpo  7503  tz7.49  8381  dfsup2  9354  supnub  9372  infnlb  9403  wofib  9457  zfregs2  9652  alephval3  10030  ac6n  10405  prmreclem5  16889  sylow1lem3  19573  ordtrest2lem  23193  trfil2  23877  alexsubALTlem3  24039  alexsubALTlem4  24040  evth  24951  lhop1lem  26005  nosupbnd1lem4  27700  vdn0conngrumgrv2  30291  nmobndseqi  30875  chpssati  32459  chrelat3  32467  nn0min  32920  xrnarchi  33272  0nellinds  33460  ordtrest2NEWlem  34113  dffr5  35989  poimirlem1  37995  poimirlem26  38020  poimirlem27  38021  fdc  38119  lpssat  39512  lssat  39515  lfl1  39569  atlrelat1  39820  unxpwdom3  43547  onsupeqnmax  43699  sucomisnotcard  43995  ss2iundf  44110  zfregs2VD  45291  rext0  45389