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  5616  supeq123d  9406  fpwwe2lem12  10623  vdwpc  17036  ramval  17064  mreexexlemd  17696  iscat  17724  iscatd  17725  catidex  17726  gsumval2a  18739  ismnddef  18790  mndpropd  18813  isgrp  19002  isgrpd2e  19018  cayleyth  19481  psgnfval  19566  iscyg  19945  ltbval  22159  opsrval  22162  scmatval  22626  pmatcollpw3fi1lem2  22909  pmatcollpw3fi1  22910  neiptopnei  23254  is1stc  23563  2ndc1stc  23573  2ndcsep  23581  islly  23590  isnlly  23591  ucnval  24398  imasdsf1olem  24495  met2ndc  24645  evthicc  25583  elmade2  28013  addsval  28117  mulsval  28264  istrkgb  28686  istrkge  28688  istrkgld  28690  legval  28815  ishpg  28996  plngval  29013  lnssplng  29028  iscgra  29073  isinag  29106  isleag  29115  nbgrval  29623  nb3grprlem2  29668  1loopgrvd0  29791  erclwwlkeq  30306  eucrctshift  30531  isplig  30765  nmoofval  31051  erlval  33515  idomsubr  33569  elrsp  33625  1arithidom  33768  dfufd2lem  33780  fldextrspunlsp  34005  extdgfialglem1  34023  constrsuc  34069  reprsuc  34943  istrkg2d  34994  iscvm  35646  cvmlift2lem13  35702  br8  36143  br6  36144  br4  36145  brsegle  36495  hilbert1.1  36541  pibp21  37944  poimirlem26  38180  poimirlem28  38182  poimirlem29  38183  cover2g  38250  isexid  38381  isrngo  38431  isrngod  38432  isgrpda  38489  lshpset  39637  cvrfval  39927  isatl  39958  ishlat1  40011  llnset  40164  lplnset  40188  lvolset  40231  lineset  40397  lcfl7N  42160  lcfrlem8  42208  lcfrlem9  42209  lcf1o  42210  hvmapffval  42417  hvmapfval  42418  hvmapval  42419  prjspval  43220  mzpcompact2lem  43367  eldioph  43374  aomclem8  43673  tfsconcatun  43949  clsk1independent  44657  ovnval  47140  sprval  48110  nnsum3primes4  48435  nnsum3primesprm  48437  nnsum3primesgbe  48439  wtgoldbnnsum4prm  48449  bgoldbnnsum3prm  48451  clnbgrval  48469  gpg3kgrtriex  48736  grlimedgnedg  48778  zlidlring  48881  uzlidlring  48882  lcoop  49069  ldepsnlinc  49166  nnpw2p  49244  lines  49389  iscnrm3r  49604