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  3084  r19.23v  3161  nfrexdw  3284  cbvrexf  3335  nfrexd  3347  rspcimedv  3579  rexab  3666  sbcrext  3836  cbvrexcsf  3905  rabn0  4352  r19.9rzv  4463  rexn0  4474  rexsng  4640  rexxfrd  5364  rexxfr2d  5366  rexxfrd2  5368  rexxfr  5371  rexiunxp  5804  rexxpf  5811  rexrnmptw  7067  rexrnmpt  7069  rexima  7212  cbvexfo  7265  rexrnmpo  7529  tz7.49  8413  dfsup2  9395  supnub  9413  infnlb  9444  wofib  9498  zfregs2  9686  alephval3  10063  ac6n  10438  prmreclem5  16891  sylow1lem3  19530  ordtrest2lem  23090  trfil2  23774  alexsubALTlem3  23936  alexsubALTlem4  23937  evth  24858  lhop1lem  25918  nosupbnd1lem4  27623  vdn0conngrumgrv2  30125  nmobndseqi  30708  chpssati  32292  chrelat3  32300  nn0min  32745  xrnarchi  33138  0nellinds  33341  ordtrest2NEWlem  33912  dffr5  35741  poimirlem1  37615  poimirlem26  37640  poimirlem27  37641  fdc  37739  lpssat  39006  lssat  39009  lfl1  39063  atlrelat1  39314  unxpwdom3  43084  onsupeqnmax  43236  sucomisnotcard  43533  ss2iundf  43648  zfregs2VD  44830  rext0  44928