Theorem dfrex2 2908

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 2903	. 2
2	1	con2bii 332	1

Syntax hints:  -.wn 3  <->wb 184  A.wral 2807  E.wrex 2808

This theorem is referenced by:  rexanali  2910  nfrexd  2919  nfrexOLD  2921  rexim  2922  r19.23v  2937  r19.30  3002  r19.35  3004  cbvrexf  3079  rspcimedv  3212  sbcrextOLD  3409  sbcrext  3410  cbvrexcsf  3467  r19.9rzv  3923  rexxfrd  4667  rexxfr2d  4669  rexxfr  4672  rexiunxp  5148  rexxpf  5155  rexrnmpt  6041  cbvexfo  6193  rexrnmpt2  6418  tz7.49  7129  dfsup2  7922  supnub  7942  wofib  7991  zfregs2  8185  alephval3  8512  ac6n  8886  prmreclem5  14438  sylow1lem3  16620  ordtrest2lem  19704  trfil2  20388  alexsubALTlem3  20549  alexsubALTlem4  20550  evth  21459  lhop1lem  22414  nmobndseqi  25694  chpssati  27282  chrelat3  27290  nn0min  27611  xrnarchi  27728  ordtrest2NEWlem  27904  dffr5  29182  fdc  30238  unxpwdom3  31041  rexxfrd2  32304  zfregs2VD  33641  lpssat  34738  lssat  34741  lfl1  34795  atlrelat1  35046

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813