Theorem rexeqbidv 3315

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 2182 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 2820	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	anbi12d 632	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3154	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-rex 3059

This theorem is referenced by:  frd  5579  supeq123d  9351  fpwwe2lem12  10551  vdwpc  16906  ramval  16934  mreexexlemd  17565  iscat  17593  iscatd  17594  catidex  17595  gsumval2a  18608  ismnddef  18659  mndpropd  18682  isgrp  18867  isgrpd2e  18883  cayleyth  19342  psgnfval  19427  iscyg  19806  ltbval  21996  opsrval  21999  scmatval  22446  pmatcollpw3fi1lem2  22729  pmatcollpw3fi1  22730  neiptopnei  23074  is1stc  23383  2ndc1stc  23393  2ndcsep  23401  islly  23410  isnlly  23411  ucnval  24218  imasdsf1olem  24315  met2ndc  24465  evthicc  25414  elmade2  27840  addsval  27932  mulsval  28078  istrkgb  28476  istrkge  28478  istrkgld  28480  legval  28605  ishpg  28780  iscgra  28830  isinag  28859  isleag  28868  nbgrval  29358  nb3grprlem2  29403  1loopgrvd0  29527  erclwwlkeq  30042  eucrctshift  30267  isplig  30500  nmoofval  30786  erlval  33289  idomsubr  33340  elrsp  33402  1arithidom  33567  dfufd2lem  33579  fldextrspunlsp  33780  extdgfialglem1  33798  constrsuc  33844  reprsuc  34721  istrkg2d  34772  iscvm  35402  cvmlift2lem13  35458  br8  35899  br6  35900  br4  35901  brsegle  36251  hilbert1.1  36297  pibp21  37559  poimirlem26  37786  poimirlem28  37788  poimirlem29  37789  cover2g  37856  isexid  37987  isrngo  38037  isrngod  38038  isgrpda  38095  lshpset  39177  cvrfval  39467  isatl  39498  ishlat1  39551  llnset  39704  lplnset  39728  lvolset  39771  lineset  39937  lcfl7N  41700  lcfrlem8  41748  lcfrlem9  41749  lcf1o  41750  hvmapffval  41957  hvmapfval  41958  hvmapval  41959  prjspval  42788  mzpcompact2lem  42935  eldioph  42942  aomclem8  43245  tfsconcatun  43521  clsk1independent  44229  ovnval  46727  sprval  47667  nnsum3primes4  47976  nnsum3primesprm  47978  nnsum3primesgbe  47980  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  clnbgrval  48010  gpg3kgrtriex  48277  grlimedgnedg  48319  zlidlring  48422  uzlidlring  48423  lcoop  48599  ldepsnlinc  48696  nnpw2p  48774  lines  48919  iscnrm3r  49135