Theorem rexeqbidv 3328

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-rex 3069

This theorem is referenced by:  frd  5539  supeq123d  9139  fpwwe2lem12  10329  vdwpc  16609  ramval  16637  mreexexlemd  17270  iscat  17298  iscatd  17299  catidex  17300  gsumval2a  18284  ismnddef  18302  mndpropd  18325  isgrp  18498  isgrpd2e  18513  cayleyth  18938  psgnfval  19023  iscyg  19394  ltbval  21154  opsrval  21157  scmatval  21561  pmatcollpw3fi1lem2  21844  pmatcollpw3fi1  21845  neiptopnei  22191  is1stc  22500  2ndc1stc  22510  2ndcsep  22518  islly  22527  isnlly  22528  ucnval  23337  imasdsf1olem  23434  met2ndc  23585  evthicc  24528  istrkgld  26724  legval  26849  ishpg  27024  iscgra  27074  isinag  27103  isleag  27112  nbgrval  27606  nb3grprlem2  27651  1loopgrvd0  27774  erclwwlkeq  28283  eucrctshift  28508  isplig  28739  nmoofval  29025  elrsp  31471  reprsuc  32495  istrkg2d  32546  iscvm  33121  cvmlift2lem13  33177  br8  33629  br6  33630  br4  33631  elmade2  33979  addsval  34053  brsegle  34337  hilbert1.1  34383  pibp21  35513  poimirlem26  35730  poimirlem28  35732  poimirlem29  35733  cover2g  35800  isexid  35932  isrngo  35982  isrngod  35983  isgrpda  36040  lshpset  36919  cvrfval  37209  isatl  37240  ishlat1  37293  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  lcfl7N  39442  lcfrlem8  39490  lcfrlem9  39491  lcf1o  39492  hvmapffval  39699  hvmapfval  39700  hvmapval  39701  prjspval  40363  mzpcompact2lem  40489  eldioph  40496  aomclem8  40802  clsk1independent  41545  ovnval  43969  sprval  44819  nnsum3primes4  45128  nnsum3primesprm  45130  nnsum3primesgbe  45132  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  zlidlring  45374  uzlidlring  45375  lcoop  45640  ldepsnlinc  45737  nnpw2p  45820  lines  45965  iscnrm3r  46130