Theorem dfrex2 3166

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

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wral 3063  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexim  3168  rexbiOLD  3170  rexanali  3191  r19.23v  3207  nfrexd  3235  nfrexdg  3236  cbvrexfw  3360  cbvrexf  3362  rspcimedv  3542  rexab  3624  sbcrext  3802  cbvrexcsf  3874  rabn0  4316  r19.9rzv  4427  rexn0  4438  rexsng  4607  rexxfrd  5327  rexxfr2d  5329  rexxfrd2  5331  rexxfr  5334  rexiunxp  5738  rexxpf  5745  rexrnmptw  6953  rexrnmpt  6955  cbvexfo  7142  rexrnmpo  7391  tz7.49  8246  dfsup2  9133  supnub  9151  infnlb  9181  wofib  9234  zfregs2  9422  alephval3  9797  ac6n  10172  prmreclem5  16549  sylow1lem3  19120  ordtrest2lem  22262  trfil2  22946  alexsubALTlem3  23108  alexsubALTlem4  23109  evth  24028  lhop1lem  25082  vdn0conngrumgrv2  28461  nmobndseqi  29042  chpssati  30626  chrelat3  30634  nn0min  31036  xrnarchi  31340  0nellinds  31468  ordtrest2NEWlem  31774  dffr5  33627  nosupbnd1lem4  33841  poimirlem1  35705  poimirlem26  35730  poimirlem27  35731  fdc  35830  lpssat  36954  lssat  36957  lfl1  37011  atlrelat1  37262  unxpwdom3  40836  ss2iundf  41156  zfregs2VD  42350