Theorem raleq 3054

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Assertion

Ref	Expression
raleq

Distinct variable groups:   ,   ,

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2
2		nfcv 2619	. 2
3	1, 2	raleqf 3050	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  A.wral 2807

This theorem is referenced by:  raleqi  3058  raleqdv  3060  raleqbi1dv  3062  sbralie  3097  r19.2zb  3919  inteq  4289  iineq1  4345  reusv6OLD  4663  reusv7OLD  4664  fri  4846  frsn  5075  fncnv  5657  isoeq4  6218  onminex  6642  tfinds  6694  f1oweALT  6784  frxp  6910  tfrlem1  7064  tfrlem12  7077  omeulem1  7250  ixpeq1  7500  undifixp  7525  ac6sfi  7784  frfi  7785  iunfi  7828  indexfi  7848  supeq1  7925  supeq2  7928  bnd2  8332  acneq  8445  aceq3lem  8522  dfac5lem4  8528  dfac8  8536  dfac9  8537  kmlem1  8551  kmlem10  8560  kmlem13  8563  cfval  8648  axcc2lem  8837  axcc4dom  8842  axdc3lem3  8853  axdc3lem4  8854  ac4c  8877  ac5  8878  ac6sg  8889  zorn2lem7  8903  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  fsuppmapnn0fiubex  12098  rexanuz  13178  rexfiuz  13180  modfsummod  13608  gcdcllem3  14151  isprs  15559  drsdirfi  15567  isdrs2  15568  ispos  15576  lubeldm  15611  lubval  15614  glbeldm  15624  glbval  15627  istos  15665  pospropd  15764  isdlat  15823  mhmpropd  15972  isghm  16267  cntzval  16359  efgval  16735  iscmn  16805  dfrhm2  17366  lidldvgen  17903  coe1fzgsumd  18344  evl1gsumd  18393  ocvval  18698  isobs  18751  mat0dimcrng  18972  mdetunilem9  19122  ist0  19821  cmpcovf  19891  is1stc  19942  2ndc1stc  19952  isref  20010  txflf  20507  ustuqtop4  20747  iscfilu  20791  ispsmet  20808  ismet  20826  isxmet  20827  cncfval  21392  lebnumlem3  21463  fmcfil  21711  iscfil3  21712  caucfil  21722  iscmet3  21732  cfilres  21735  minveclem3  21844  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  dvcn  22324  ulmval  22775  axtgcont1  23865  nb3grapr  24453  rusgrasn  24945  isplig  25179  isgrpo  25198  isablo  25285  isexid2  25327  ismndo2  25347  rngomndo  25423  ocval  26198  isomnd  27691  isorng  27789  ismbfm  28223  isanmbfm  28227  derangval  28611  setinds  29210  dfon2lem3  29217  dfon2lem7  29221  tfisg  29284  poseq  29333  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  sltval2  29416  sltres  29424  nodense  29449  nobndup  29460  nobnddown  29461  nofulllem1  29462  dfrdg4  29600  tfrqfree  29601  finixpnum  30038  mblfinlem1  30051  mbfresfi  30061  isfne  30157  indexdom  30225  heibor1lem  30305  pridl  30434  smprngopr  30449  ispridlc  30467  setindtrs  30967  dford3lem2  30969  dfac11  31008  fnchoice  31404  raleqd  31440  stoweidlem31  31813  stoweidlem57  31839  fourierdlem80  31969  fourierdlem103  31992  fourierdlem104  31993  mgmhmpropd  32473  rnghmval  32697  zrrnghm  32723  bnj865  33981  bnj1154  34055  bnj1296  34077  bnj1463  34111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812