Theorem dfrex2 3239

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

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wral 3138  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  rexim  3241  rexanali  3265  r19.23v  3279  nfrexd  3307  nfrexdg  3308  r19.30OLD  3339  cbvrexfw  3438  cbvrexf  3440  rspcimedv  3613  sbcrext  3855  cbvrexcsf  3925  rabn0  4338  r19.9rzv  4444  rexxfrd  5301  rexxfr2d  5303  rexxfrd2  5305  rexxfr  5308  rexiunxp  5705  rexxpf  5712  rexrnmptw  6855  rexrnmpt  6857  cbvexfo  7040  rexrnmpo  7284  tz7.49  8075  dfsup2  8902  supnub  8920  infnlb  8950  wofib  9003  zfregs2  9169  alephval3  9530  ac6n  9901  prmreclem5  16250  sylow1lem3  18719  ordtrest2lem  21805  trfil2  22489  alexsubALTlem3  22651  alexsubALTlem4  22652  evth  23557  lhop1lem  24604  vdn0conngrumgrv2  27969  nmobndseqi  28550  chpssati  30134  chrelat3  30142  nn0min  30531  xrnarchi  30808  0nellinds  30930  ordtrest2NEWlem  31160  dffr5  32984  nosupbnd1lem4  33206  poimirlem1  34887  poimirlem26  34912  poimirlem27  34913  fdc  35014  lpssat  36143  lssat  36146  lfl1  36200  atlrelat1  36451  unxpwdom3  39688  ss2iundf  39997  zfregs2VD  41168