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

Theorem rexeqbidv 3292
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 3284 . 2 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rexbidv 3190 . 2 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑥𝐵 𝜒))
52, 4bitrd 268 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wrex 3051
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 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-ext 2740
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 2753  df-clel 2756  df-nfc 2891  df-rex 3056
This theorem is referenced by:  supeq123d  8521  fpwwe2lem13  9656  hashge2el2difr  13455  vdwpc  15886  ramval  15914  mreexexlemd  16506  iscat  16534  iscatd  16535  catidex  16536  gsumval2a  17480  ismnddef  17497  mndpropd  17517  isgrp  17629  isgrpd2e  17642  cayleyth  18035  psgnfval  18120  iscyg  18481  ltbval  19673  opsrval  19676  scmatval  20512  pmatcollpw3fi1lem2  20794  pmatcollpw3fi1  20795  neiptopnei  21138  is1stc  21446  2ndc1stc  21456  2ndcsep  21464  islly  21473  isnlly  21474  ucnval  22282  imasdsf1olem  22379  met2ndc  22529  evthicc  23428  istrkgld  25557  legval  25678  ishpg  25850  iscgra  25900  isinag  25928  isleag  25932  nbgrval  26428  nb3grprlem2  26481  1loopgrvd0  26610  erclwwlkeq  27141  eucrctshift  27395  isplig  27639  nmoofval  27926  reprsuc  31002  istrkg2d  31053  iscvm  31548  cvmlift2lem13  31604  br8  31953  br6  31954  br4  31955  brsegle  32521  hilbert1.1  32567  poimirlem26  33748  poimirlem28  33750  poimirlem29  33751  cover2g  33822  isexid  33959  isrngo  34009  isrngod  34010  isgrpda  34067  lshpset  34768  cvrfval  35058  isatl  35089  ishlat1  35142  llnset  35294  lplnset  35318  lvolset  35361  lineset  35527  lcfl7N  37292  lcfrlem8  37340  lcfrlem9  37341  lcf1o  37342  hvmapffval  37549  hvmapfval  37550  hvmapval  37551  mzpcompact2lem  37816  eldioph  37823  aomclem8  38133  clsk1independent  38846  ovnval  41261  nnsum3primes4  42186  nnsum3primesprm  42188  nnsum3primesgbe  42190  wtgoldbnnsum4prm  42200  bgoldbnnsum3prm  42202  sprval  42239  zlidlring  42438  uzlidlring  42439  lcoop  42710  ldepsnlinc  42807  nnpw2p  42890
  Copyright terms: Public domain W3C validator