Theorem rexeqbidv 3310

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2142, ax-11 2158, and ax-12 2178 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 2814	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	anbi12d 632	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3149	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  frd  5576  supeq123d  9340  fpwwe2lem12  10536  vdwpc  16892  ramval  16920  mreexexlemd  17550  iscat  17578  iscatd  17579  catidex  17580  gsumval2a  18559  ismnddef  18610  mndpropd  18633  isgrp  18818  isgrpd2e  18834  cayleyth  19294  psgnfval  19379  iscyg  19758  ltbval  21948  opsrval  21951  scmatval  22389  pmatcollpw3fi1lem2  22672  pmatcollpw3fi1  22673  neiptopnei  23017  is1stc  23326  2ndc1stc  23336  2ndcsep  23344  islly  23353  isnlly  23354  ucnval  24162  imasdsf1olem  24259  met2ndc  24409  evthicc  25358  elmade2  27782  addsval  27874  mulsval  28017  istrkgb  28400  istrkge  28402  istrkgld  28404  legval  28529  ishpg  28704  iscgra  28754  isinag  28783  isleag  28792  nbgrval  29281  nb3grprlem2  29326  1loopgrvd0  29450  erclwwlkeq  29962  eucrctshift  30187  isplig  30420  nmoofval  30706  erlval  33198  idomsubr  33248  elrsp  33309  1arithidom  33474  dfufd2lem  33486  fldextrspunlsp  33641  extdgfialglem1  33659  constrsuc  33705  reprsuc  34583  istrkg2d  34634  iscvm  35232  cvmlift2lem13  35288  br8  35729  br6  35730  br4  35731  brsegle  36082  hilbert1.1  36128  pibp21  37389  poimirlem26  37626  poimirlem28  37628  poimirlem29  37629  cover2g  37696  isexid  37827  isrngo  37877  isrngod  37878  isgrpda  37935  lshpset  38957  cvrfval  39247  isatl  39278  ishlat1  39331  llnset  39484  lplnset  39508  lvolset  39551  lineset  39717  lcfl7N  41480  lcfrlem8  41528  lcfrlem9  41529  lcf1o  41530  hvmapffval  41737  hvmapfval  41738  hvmapval  41739  prjspval  42576  mzpcompact2lem  42724  eldioph  42731  aomclem8  43034  tfsconcatun  43310  clsk1independent  44019  ovnval  46522  sprval  47463  nnsum3primes4  47772  nnsum3primesprm  47774  nnsum3primesgbe  47776  wtgoldbnnsum4prm  47786  bgoldbnnsum3prm  47788  clnbgrval  47806  gpg3kgrtriex  48073  grlimedgnedg  48115  zlidlring  48218  uzlidlring  48219  lcoop  48396  ldepsnlinc  48493  nnpw2p  48571  lines  48716  iscnrm3r  48932