Theorem rexeqbidv 3317

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 3153	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  5588  supeq123d  9377  fpwwe2lem12  10571  vdwpc  16927  ramval  16955  mreexexlemd  17585  iscat  17613  iscatd  17614  catidex  17615  gsumval2a  18594  ismnddef  18645  mndpropd  18668  isgrp  18853  isgrpd2e  18869  cayleyth  19329  psgnfval  19414  iscyg  19793  ltbval  21983  opsrval  21986  scmatval  22424  pmatcollpw3fi1lem2  22707  pmatcollpw3fi1  22708  neiptopnei  23052  is1stc  23361  2ndc1stc  23371  2ndcsep  23379  islly  23388  isnlly  23389  ucnval  24197  imasdsf1olem  24294  met2ndc  24444  evthicc  25393  elmade2  27817  addsval  27909  mulsval  28052  istrkgb  28435  istrkge  28437  istrkgld  28439  legval  28564  ishpg  28739  iscgra  28789  isinag  28818  isleag  28827  nbgrval  29316  nb3grprlem2  29361  1loopgrvd0  29485  erclwwlkeq  29997  eucrctshift  30222  isplig  30455  nmoofval  30741  erlval  33225  idomsubr  33275  elrsp  33336  1arithidom  33501  dfufd2lem  33513  fldextrspunlsp  33662  constrsuc  33721  reprsuc  34599  istrkg2d  34650  iscvm  35239  cvmlift2lem13  35295  br8  35736  br6  35737  br4  35738  brsegle  36089  hilbert1.1  36135  pibp21  37396  poimirlem26  37633  poimirlem28  37635  poimirlem29  37636  cover2g  37703  isexid  37834  isrngo  37884  isrngod  37885  isgrpda  37942  lshpset  38964  cvrfval  39254  isatl  39285  ishlat1  39338  llnset  39492  lplnset  39516  lvolset  39559  lineset  39725  lcfl7N  41488  lcfrlem8  41536  lcfrlem9  41537  lcf1o  41538  hvmapffval  41745  hvmapfval  41746  hvmapval  41747  prjspval  42584  mzpcompact2lem  42732  eldioph  42739  aomclem8  43043  tfsconcatun  43319  clsk1independent  44028  ovnval  46532  sprval  47473  nnsum3primes4  47782  nnsum3primesprm  47784  nnsum3primesgbe  47786  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  clnbgrval  47816  gpg3kgrtriex  48073  zlidlring  48215  uzlidlring  48216  lcoop  48393  ldepsnlinc  48490  nnpw2p  48568  lines  48713  iscnrm3r  48929