Theorem dfrex2 3060

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3048  ∃wrex 3057

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3049  df-rex 3058

This theorem is referenced by:  rexanali  3087  r19.23v  3160  nfrexdw  3279  cbvrexf  3328  nfrexd  3340  rspcimedv  3564  rexab  3650  sbcrext  3820  cbvrexcsf  3889  rabn0  4338  r19.9rzv  4449  rexn0  4460  rexsng  4628  rexxfrd  5349  rexxfr2d  5351  rexxfrd2  5353  rexxfr  5356  rexiunxp  5784  rexxpf  5791  rexrnmptw  7034  rexrnmpt  7036  rexima  7178  cbvexfo  7230  rexrnmpo  7492  tz7.49  8370  dfsup2  9335  supnub  9353  infnlb  9384  wofib  9438  zfregs2  9630  alephval3  10008  ac6n  10383  prmreclem5  16834  sylow1lem3  19514  ordtrest2lem  23119  trfil2  23803  alexsubALTlem3  23965  alexsubALTlem4  23966  evth  24886  lhop1lem  25946  nosupbnd1lem4  27651  vdn0conngrumgrv2  30178  nmobndseqi  30761  chpssati  32345  chrelat3  32353  nn0min  32808  xrnarchi  33160  0nellinds  33342  ordtrest2NEWlem  33956  dffr5  35819  poimirlem1  37681  poimirlem26  37706  poimirlem27  37707  fdc  37805  lpssat  39132  lssat  39135  lfl1  39189  atlrelat1  39440  unxpwdom3  43212  onsupeqnmax  43364  sucomisnotcard  43661  ss2iundf  43776  zfregs2VD  44957  rext0  45055