Theorem dfrex2 3063

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3051  ∃wrex 3060

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 3052  df-rex 3061

This theorem is referenced by:  rexanali  3090  r19.23v  3163  nfrexdw  3282  cbvrexf  3331  nfrexd  3343  rspcimedv  3567  rexab  3653  sbcrext  3823  cbvrexcsf  3892  rabn0  4341  rexn0  4449  r19.9rzv  4458  rexsng  4633  rexxfrd  5354  rexxfr2d  5356  rexxfrd2  5358  rexxfr  5361  rexiunxp  5789  rexxpf  5796  rexrnmptw  7040  rexrnmpt  7042  rexima  7184  cbvexfo  7236  rexrnmpo  7498  tz7.49  8376  dfsup2  9347  supnub  9365  infnlb  9396  wofib  9450  zfregs2  9642  alephval3  10020  ac6n  10395  prmreclem5  16848  sylow1lem3  19529  ordtrest2lem  23147  trfil2  23831  alexsubALTlem3  23993  alexsubALTlem4  23994  evth  24914  lhop1lem  25974  nosupbnd1lem4  27679  vdn0conngrumgrv2  30271  nmobndseqi  30854  chpssati  32438  chrelat3  32446  nn0min  32901  xrnarchi  33266  0nellinds  33451  ordtrest2NEWlem  34079  dffr5  35948  poimirlem1  37818  poimirlem26  37843  poimirlem27  37844  fdc  37942  lpssat  39269  lssat  39272  lfl1  39326  atlrelat1  39577  unxpwdom3  43333  onsupeqnmax  43485  sucomisnotcard  43781  ss2iundf  43896  zfregs2VD  45077  rext0  45175