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

Theorem rexeqbidv 3142
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 3134 . 2 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rexbidv 3045 . 2 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑥𝐵 𝜒))
52, 4bitrd 268 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913
This theorem is referenced by:  supeq123d  8300  fpwwe2lem13  9408  hashge2el2difr  13201  vdwpc  15608  ramval  15636  mreexexlemd  16225  iscat  16254  iscatd  16255  catidex  16256  gsumval2a  17200  ismnddef  17217  mndpropd  17237  isgrp  17349  isgrpd2e  17362  cayleyth  17756  psgnfval  17841  iscyg  18202  ltbval  19390  opsrval  19393  scmatval  20229  pmatcollpw3fi1lem2  20511  pmatcollpw3fi1  20512  neiptopnei  20846  is1stc  21154  2ndc1stc  21164  2ndcsep  21172  islly  21181  isnlly  21182  ucnval  21991  imasdsf1olem  22088  met2ndc  22238  evthicc  23135  istrkgld  25258  legval  25379  ishpg  25551  iscgra  25601  isinag  25629  isleag  25633  nbgrval  26121  nb3grprlem2  26170  1loopgrvd0  26286  erclwwlkseq  26798  eucrctshift  26969  isplig  27182  nmoofval  27466  istrkg2d  30451  iscvm  30949  cvmlift2lem13  31005  br8  31354  br6  31355  br4  31356  brsegle  31857  hilbert1.1  31903  poimirlem26  33067  poimirlem28  33069  poimirlem29  33070  cover2g  33141  isexid  33278  isrngo  33328  isrngod  33329  isgrpda  33386  lshpset  33745  cvrfval  34035  isatl  34066  ishlat1  34119  llnset  34271  lplnset  34295  lvolset  34338  lineset  34504  lcfl7N  36270  lcfrlem8  36318  lcfrlem9  36319  lcf1o  36320  hvmapffval  36527  hvmapfval  36528  hvmapval  36529  mzpcompact2lem  36794  eldioph  36801  aomclem8  37111  clsk1independent  37826  ovnval  40062  nnsum3primes4  40965  nnsum3primesprm  40967  nnsum3primesgbe  40969  wtgoldbnnsum4prm  40979  bgoldbnnsum3prm  40981  sprval  41017  zlidlring  41216  uzlidlring  41217  lcoop  41488  ldepsnlinc  41585  nnpw2p  41672
  Copyright terms: Public domain W3C validator