Theorem rexeqbidv 3313

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-rex 3057

This theorem is referenced by:  frd  5571  supeq123d  9334  fpwwe2lem12  10533  vdwpc  16892  ramval  16920  mreexexlemd  17550  iscat  17578  iscatd  17579  catidex  17580  gsumval2a  18593  ismnddef  18644  mndpropd  18667  isgrp  18852  isgrpd2e  18868  cayleyth  19327  psgnfval  19412  iscyg  19791  ltbval  21978  opsrval  21981  scmatval  22419  pmatcollpw3fi1lem2  22702  pmatcollpw3fi1  22703  neiptopnei  23047  is1stc  23356  2ndc1stc  23366  2ndcsep  23374  islly  23383  isnlly  23384  ucnval  24191  imasdsf1olem  24288  met2ndc  24438  evthicc  25387  elmade2  27813  addsval  27905  mulsval  28048  istrkgb  28433  istrkge  28435  istrkgld  28437  legval  28562  ishpg  28737  iscgra  28787  isinag  28816  isleag  28825  nbgrval  29314  nb3grprlem2  29359  1loopgrvd0  29483  erclwwlkeq  29998  eucrctshift  30223  isplig  30456  nmoofval  30742  erlval  33225  idomsubr  33275  elrsp  33337  1arithidom  33502  dfufd2lem  33514  fldextrspunlsp  33687  extdgfialglem1  33705  constrsuc  33751  reprsuc  34628  istrkg2d  34679  iscvm  35303  cvmlift2lem13  35359  br8  35800  br6  35801  br4  35802  brsegle  36152  hilbert1.1  36198  pibp21  37459  poimirlem26  37696  poimirlem28  37698  poimirlem29  37699  cover2g  37766  isexid  37897  isrngo  37947  isrngod  37948  isgrpda  38005  lshpset  39087  cvrfval  39377  isatl  39408  ishlat1  39461  llnset  39614  lplnset  39638  lvolset  39681  lineset  39847  lcfl7N  41610  lcfrlem8  41658  lcfrlem9  41659  lcf1o  41660  hvmapffval  41867  hvmapfval  41868  hvmapval  41869  prjspval  42706  mzpcompact2lem  42854  eldioph  42861  aomclem8  43164  tfsconcatun  43440  clsk1independent  44149  ovnval  46649  sprval  47589  nnsum3primes4  47898  nnsum3primesprm  47900  nnsum3primesgbe  47902  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  clnbgrval  47932  gpg3kgrtriex  48199  grlimedgnedg  48241  zlidlring  48344  uzlidlring  48345  lcoop  48522  ldepsnlinc  48619  nnpw2p  48697  lines  48842  iscnrm3r  49058