Theorem dfrex2 3079

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

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wral 3067  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  rexanali  3108  rexbiOLD  3111  r19.23v  3189  nfrexdw  3316  cbvrexf  3369  nfrexd  3381  rspcimedv  3626  rexab  3716  sbcrext  3895  cbvrexcsf  3967  rabn0  4412  r19.9rzv  4523  rexn0  4534  rexsng  4698  rexxfrd  5427  rexxfr2d  5429  rexxfrd2  5431  rexxfr  5434  rexiunxp  5865  rexxpf  5872  rexrnmptw  7129  rexrnmpt  7131  rexima  7275  cbvexfo  7326  rexrnmpo  7590  tz7.49  8501  dfsup2  9513  supnub  9531  infnlb  9561  wofib  9614  zfregs2  9802  alephval3  10179  ac6n  10554  prmreclem5  16967  sylow1lem3  19642  ordtrest2lem  23232  trfil2  23916  alexsubALTlem3  24078  alexsubALTlem4  24079  evth  25010  lhop1lem  26072  nosupbnd1lem4  27774  vdn0conngrumgrv2  30228  nmobndseqi  30811  chpssati  32395  chrelat3  32403  nn0min  32824  xrnarchi  33164  0nellinds  33363  ordtrest2NEWlem  33868  dffr5  35716  poimirlem1  37581  poimirlem26  37606  poimirlem27  37607  fdc  37705  lpssat  38969  lssat  38972  lfl1  39026  atlrelat1  39277  unxpwdom3  43052  onsupeqnmax  43208  sucomisnotcard  43506  ss2iundf  43621  zfregs2VD  44812