Theorem rexeqbidv 3346

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2182, ax-11 2198, and ax-12 2219 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

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eleq2d 2855	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	anbi12d 643	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3191	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-rex 3096

This theorem is referenced by:  frd  5619  supeq123d  9409  fpwwe2lem12  10626  vdwpc  17039  ramval  17067  mreexexlemd  17699  iscat  17727  iscatd  17728  catidex  17729  gsumval2a  18742  ismnddef  18793  mndpropd  18816  isgrp  19005  isgrpd2e  19021  cayleyth  19484  psgnfval  19569  iscyg  19948  ltbval  22162  opsrval  22165  scmatval  22629  pmatcollpw3fi1lem2  22912  pmatcollpw3fi1  22913  neiptopnei  23257  is1stc  23566  2ndc1stc  23576  2ndcsep  23584  islly  23593  isnlly  23594  ucnval  24401  imasdsf1olem  24498  met2ndc  24648  evthicc  25586  elmade2  28016  addsval  28120  mulsval  28267  istrkgb  28689  istrkge  28691  istrkgld  28693  legval  28818  ishpg  28999  plngval  29016  lnssplng  29031  iscgra  29076  isinag  29109  isleag  29118  nbgrval  29626  nb3grprlem2  29671  1loopgrvd0  29794  erclwwlkeq  30309  eucrctshift  30534  isplig  30768  nmoofval  31054  erlval  33518  idomsubr  33572  elrsp  33628  1arithidom  33771  dfufd2lem  33783  fldextrspunlsp  34008  extdgfialglem1  34026  constrsuc  34072  reprsuc  34946  istrkg2d  34997  iscvm  35649  cvmlift2lem13  35705  br8  36146  br6  36147  br4  36148  brsegle  36498  hilbert1.1  36544  pibp21  37948  poimirlem26  38184  poimirlem28  38186  poimirlem29  38187  cover2g  38254  isexid  38385  isrngo  38435  isrngod  38436  isgrpda  38493  lshpset  39641  cvrfval  39931  isatl  39962  ishlat1  40015  llnset  40168  lplnset  40192  lvolset  40235  lineset  40401  lcfl7N  42164  lcfrlem8  42212  lcfrlem9  42213  lcf1o  42214  hvmapffval  42421  hvmapfval  42422  hvmapval  42423  prjspval  43226  mzpcompact2lem  43373  eldioph  43380  aomclem8  43679  tfsconcatun  43955  clsk1independent  44663  ovnval  47146  sprval  48116  nnsum3primes4  48441  nnsum3primesprm  48443  nnsum3primesgbe  48445  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  clnbgrval  48475  gpg3kgrtriex  48742  grlimedgnedg  48784  zlidlring  48887  uzlidlring  48888  lcoop  49075  ldepsnlinc  49172  nnpw2p  49250  lines  49395  iscnrm3r  49610