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

Theorem rexeqbidv 3393
 Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2146, ax-11 2162, and ax-12 2179 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.)
Hypotheses
Ref Expression
raleqbidv.1 (𝜑𝐴 = 𝐵)
raleqbidv.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rexeqbidv (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem rexeqbidv
StepHypRef Expression
1 raleqbidv.1 . . . 4 (𝜑𝐴 = 𝐵)
21eleq2d 2901 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
3 raleqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
42, 3anbi12d 633 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐵𝜒)))
54rexbidv2 3287 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2115  ∃wrex 3134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-rex 3139 This theorem is referenced by:  rexeqbi1dv  3395  supeq123d  8913  fpwwe2lem13  10064  vdwpc  16316  ramval  16344  mreexexlemd  16917  iscat  16945  iscatd  16946  catidex  16947  gsumval2a  17897  ismnddef  17915  mndpropd  17938  isgrp  18111  isgrpd2e  18124  cayleyth  18545  psgnfval  18630  iscyg  19000  ltbval  20720  opsrval  20723  scmatval  21118  pmatcollpw3fi1lem2  21401  pmatcollpw3fi1  21402  neiptopnei  21746  is1stc  22055  2ndc1stc  22065  2ndcsep  22073  islly  22082  isnlly  22083  ucnval  22892  imasdsf1olem  22989  met2ndc  23139  evthicc  24072  istrkgld  26262  legval  26387  ishpg  26562  iscgra  26612  isinag  26641  isleag  26650  nbgrval  27135  nb3grprlem2  27180  1loopgrvd0  27303  erclwwlkeq  27812  eucrctshift  28037  isplig  28268  nmoofval  28554  elrsp  30981  reprsuc  31971  istrkg2d  32022  iscvm  32591  cvmlift2lem13  32647  br8  33077  br6  33078  br4  33079  brsegle  33654  hilbert1.1  33700  pibp21  34804  poimirlem26  35055  poimirlem28  35057  poimirlem29  35058  cover2g  35125  isexid  35257  isrngo  35307  isrngod  35308  isgrpda  35365  lshpset  36246  cvrfval  36536  isatl  36567  ishlat1  36620  llnset  36773  lplnset  36797  lvolset  36840  lineset  37006  lcfl7N  38769  lcfrlem8  38817  lcfrlem9  38818  lcf1o  38819  hvmapffval  39026  hvmapfval  39027  hvmapval  39028  prjspval  39541  mzpcompact2lem  39636  eldioph  39643  aomclem8  39949  clsk1independent  40696  ovnval  43133  sprval  43949  nnsum3primes4  44259  nnsum3primesprm  44261  nnsum3primesgbe  44263  wtgoldbnnsum4prm  44273  bgoldbnnsum3prm  44275  zlidlring  44505  uzlidlring  44506  lcoop  44773  ldepsnlinc  44870  nnpw2p  44953  lines  45098
 Copyright terms: Public domain W3C validator