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

Theorem rexeqbidv 3342
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:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rexeqbidv
StepHypRef Expression
1 raleqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
21rexeqdv 3334 . 2 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rexbidv 3240 . 2 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑥𝐵 𝜒))
52, 4bitrd 270 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102
This theorem is referenced by:  supeq123d  8591  fpwwe2lem13  9745  hashge2el2difr  13476  vdwpc  15897  ramval  15925  mreexexlemd  16505  iscat  16533  iscatd  16534  catidex  16535  gsumval2a  17480  ismnddef  17497  mndpropd  17517  isgrp  17629  isgrpd2e  17642  cayleyth  18032  psgnfval  18117  iscyg  18478  ltbval  19676  opsrval  19679  scmatval  20518  pmatcollpw3fi1lem2  20802  pmatcollpw3fi1  20803  neiptopnei  21147  is1stc  21455  2ndc1stc  21465  2ndcsep  21473  islly  21482  isnlly  21483  ucnval  22291  imasdsf1olem  22388  met2ndc  22538  evthicc  23439  istrkgld  25571  legval  25692  ishpg  25864  iscgra  25914  isinag  25942  isleag  25946  nbgrval  26444  nb3grprlem2  26498  1loopgrvd0  26627  erclwwlkeq  27160  eucrctshift  27415  isplig  27658  nmoofval  27944  reprsuc  31017  istrkg2d  31068  iscvm  31562  cvmlift2lem13  31618  br8  31966  br6  31967  br4  31968  brsegle  32534  hilbert1.1  32580  poimirlem26  33746  poimirlem28  33748  poimirlem29  33749  cover2g  33819  isexid  33955  isrngo  34005  isrngod  34006  isgrpda  34063  lshpset  34756  cvrfval  35046  isatl  35077  ishlat1  35130  llnset  35283  lplnset  35307  lvolset  35350  lineset  35516  lcfl7N  37279  lcfrlem8  37327  lcfrlem9  37328  lcf1o  37329  hvmapffval  37536  hvmapfval  37537  hvmapval  37538  mzpcompact2lem  37813  eldioph  37820  aomclem8  38129  clsk1independent  38841  ovnval  41234  nnsum3primes4  42248  nnsum3primesprm  42250  nnsum3primesgbe  42252  wtgoldbnnsum4prm  42262  bgoldbnnsum3prm  42264  sprval  42294  zlidlring  42493  uzlidlring  42494  lcoop  42765  ldepsnlinc  42862  nnpw2p  42945
  Copyright terms: Public domain W3C validator