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

Theorem rexeqbidv 3293
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 3285 . 2 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rexbidv 3191 . 2 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑥𝐵 𝜒))
52, 4bitrd 268 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wrex 3052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rex 3057
This theorem is referenced by:  supeq123d  8524  fpwwe2lem13  9677  hashge2el2difr  13476  vdwpc  15907  ramval  15935  mreexexlemd  16527  iscat  16555  iscatd  16556  catidex  16557  gsumval2a  17501  ismnddef  17518  mndpropd  17538  isgrp  17650  isgrpd2e  17663  cayleyth  18056  psgnfval  18141  iscyg  18502  ltbval  19694  opsrval  19697  scmatval  20533  pmatcollpw3fi1lem2  20815  pmatcollpw3fi1  20816  neiptopnei  21159  is1stc  21467  2ndc1stc  21477  2ndcsep  21485  islly  21494  isnlly  21495  ucnval  22303  imasdsf1olem  22400  met2ndc  22550  evthicc  23449  istrkgld  25579  legval  25700  ishpg  25872  iscgra  25922  isinag  25950  isleag  25954  nbgrval  26450  nb3grprlem2  26503  1loopgrvd0  26632  erclwwlkeq  27163  eucrctshift  27417  isplig  27661  nmoofval  27948  reprsuc  31024  istrkg2d  31075  iscvm  31570  cvmlift2lem13  31626  br8  31975  br6  31976  br4  31977  brsegle  32543  hilbert1.1  32589  poimirlem26  33767  poimirlem28  33769  poimirlem29  33770  cover2g  33841  isexid  33978  isrngo  34028  isrngod  34029  isgrpda  34086  lshpset  34787  cvrfval  35077  isatl  35108  ishlat1  35161  llnset  35313  lplnset  35337  lvolset  35380  lineset  35546  lcfl7N  37311  lcfrlem8  37359  lcfrlem9  37360  lcf1o  37361  hvmapffval  37568  hvmapfval  37569  hvmapval  37570  mzpcompact2lem  37835  eldioph  37842  aomclem8  38152  clsk1independent  38865  ovnval  41280  nnsum3primes4  42205  nnsum3primesprm  42207  nnsum3primesgbe  42209  wtgoldbnnsum4prm  42219  bgoldbnnsum3prm  42221  sprval  42258  zlidlring  42457  uzlidlring  42458  lcoop  42729  ldepsnlinc  42826  nnpw2p  42909
  Copyright terms: Public domain W3C validator