MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeqbidv Unicode version

Theorem rexeqbidv 3069
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)
Hypotheses
Ref Expression
raleqbidv.1
raleqbidv.2
Assertion
Ref Expression
rexeqbidv
Distinct variable groups:   ,   ,   ,

Proof of Theorem rexeqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3
21rexeqdv 3061 . 2
3 raleqbidv.2 . . 3
43rexbidv 2968 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wrex 2808
This theorem is referenced by:  supeq123d  7930  fpwwe2lem13  9041  vdwpc  14498  ramval  14526  mreexexlemd  15041  iscat  15069  iscatd  15070  catidex  15071  gsumval2a  15906  ismnddef  15922  ismndOLD  15926  mndpropd  15946  isgrp  16061  isgrpd2e  16072  cayleyth  16440  psgnfval  16525  iscyg  16882  ltbval  18136  opsrval  18139  scmatval  19006  pmatcollpw3fi1lem2  19288  pmatcollpw3fi1  19289  neiptopnei  19633  is1stc  19942  2ndc1stc  19952  2ndcsep  19960  islly  19969  isnlly  19970  ucnval  20780  imasdsf1olem  20876  met2ndc  21026  evthicc  21871  istrkg2d  23856  istrkgld  23857  legval  23971  ishpg  24128  iscgra  24169  nb3graprlem2  24452  erclwwlkeq  24811  2wlksot  24867  2spthsot  24868  isplig  25179  isgrp2d  25237  isgrpda  25299  isexid  25319  isrngo  25380  isrngod  25381  nmoofval  25677  iscvm  28704  cvmlift2lem13  28760  br8  29185  br6  29186  br4  29187  brsegle  29758  hilbert1.1  29804  cover2g  30205  mzpcompact2lem  30684  eldioph  30691  aomclem8  31007  zlidlring  32734  uzlidlring  32735  lcoop  33012  ldepsnlinc  33109  lshpset  34703  cvrfval  34993  isatl  35024  ishlat1  35077  llnset  35229  lplnset  35253  lvolset  35296  lineset  35462  lcfl7N  37228  lcfrlem8  37276  lcfrlem9  37277  lcf1o  37278  hvmapffval  37485  hvmapfval  37486  hvmapval  37487
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-rex 2813
  Copyright terms: Public domain W3C validator