Theorem dfrex2 3025

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

Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wral 2941  ∃wrex 2942

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

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947

This theorem is referenced by:  rexanali  3027  nfrexd  3035  rexim  3037  r19.23v  3052  r19.30  3111  r19.35  3113  cbvrexf  3196  rspcimedv  3342  sbcrext  3544  sbcrextOLD  3545  cbvrexcsf  3599  rabn0  3991  r19.9rzv  4098  rexxfrd  4911  rexxfr2d  4913  rexxfrd2  4915  rexxfr  4918  rexiunxp  5295  rexxpf  5302  rexrnmpt  6409  cbvexfo  6585  rexrnmpt2  6818  tz7.49  7585  dfsup2  8391  supnub  8409  infnlb  8439  wofib  8491  zfregs2  8647  alephval3  8971  ac6n  9345  prmreclem5  15671  sylow1lem3  18061  ordtrest2lem  21055  trfil2  21738  alexsubALTlem3  21900  alexsubALTlem4  21901  evth  22805  lhop1lem  23821  vdn0conngrumgrv2  27174  nmobndseqi  27762  chpssati  29350  chrelat3  29358  nn0min  29695  xrnarchi  29866  ordtrest2NEWlem  30096  dffr5  31769  nosupbnd1lem4  31982  poimirlem1  33540  poimirlem26  33565  poimirlem27  33566  fdc  33671  lpssat  34618  lssat  34621  lfl1  34675  atlrelat1  34926  unxpwdom3  37982  ss2iundf  38268  zfregs2VD  39390