Theorem dfrex2 3056

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3044  ∃wrex 3053

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 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  rexanali  3083  r19.23v  3156  nfrexdw  3276  cbvrexf  3326  nfrexd  3338  rspcimedv  3570  rexab  3657  sbcrext  3827  cbvrexcsf  3896  rabn0  4342  r19.9rzv  4453  rexn0  4464  rexsng  4630  rexxfrd  5351  rexxfr2d  5353  rexxfrd2  5355  rexxfr  5358  rexiunxp  5787  rexxpf  5794  rexrnmptw  7033  rexrnmpt  7035  rexima  7178  cbvexfo  7231  rexrnmpo  7493  tz7.49  8374  dfsup2  9353  supnub  9371  infnlb  9402  wofib  9456  zfregs2  9648  alephval3  10023  ac6n  10398  prmreclem5  16850  sylow1lem3  19497  ordtrest2lem  23106  trfil2  23790  alexsubALTlem3  23952  alexsubALTlem4  23953  evth  24874  lhop1lem  25934  nosupbnd1lem4  27639  vdn0conngrumgrv2  30158  nmobndseqi  30741  chpssati  32325  chrelat3  32333  nn0min  32778  xrnarchi  33136  0nellinds  33317  ordtrest2NEWlem  33888  dffr5  35726  poimirlem1  37600  poimirlem26  37625  poimirlem27  37626  fdc  37724  lpssat  38991  lssat  38994  lfl1  39048  atlrelat1  39299  unxpwdom3  43068  onsupeqnmax  43220  sucomisnotcard  43517  ss2iundf  43632  zfregs2VD  44814  rext0  44912