Theorem rexeqbidv 3344

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172 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 3175	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-rex 3072

This theorem is referenced by:  frd  5636  supeq123d  9445  fpwwe2lem12  10637  vdwpc  16913  ramval  16941  mreexexlemd  17588  iscat  17616  iscatd  17617  catidex  17618  gsumval2a  18604  ismnddef  18627  mndpropd  18650  isgrp  18825  isgrpd2e  18841  cayleyth  19283  psgnfval  19368  iscyg  19747  ltbval  21598  opsrval  21601  scmatval  22006  pmatcollpw3fi1lem2  22289  pmatcollpw3fi1  22290  neiptopnei  22636  is1stc  22945  2ndc1stc  22955  2ndcsep  22963  islly  22972  isnlly  22973  ucnval  23782  imasdsf1olem  23879  met2ndc  24032  evthicc  24976  elmade2  27363  addsval  27446  mulsval  27565  istrkgb  27706  istrkge  27708  istrkgld  27710  legval  27835  ishpg  28010  iscgra  28060  isinag  28089  isleag  28098  nbgrval  28593  nb3grprlem2  28638  1loopgrvd0  28761  erclwwlkeq  29271  eucrctshift  29496  isplig  29729  nmoofval  30015  elrsp  32486  reprsuc  33627  istrkg2d  33678  iscvm  34250  cvmlift2lem13  34306  br8  34726  br6  34727  br4  34728  brsegle  35080  hilbert1.1  35126  pibp21  36296  poimirlem26  36514  poimirlem28  36516  poimirlem29  36517  cover2g  36584  isexid  36715  isrngo  36765  isrngod  36766  isgrpda  36823  lshpset  37848  cvrfval  38138  isatl  38169  ishlat1  38222  llnset  38376  lplnset  38400  lvolset  38443  lineset  38609  lcfl7N  40372  lcfrlem8  40420  lcfrlem9  40421  lcf1o  40422  hvmapffval  40629  hvmapfval  40630  hvmapval  40631  prjspval  41345  mzpcompact2lem  41489  eldioph  41496  aomclem8  41803  tfsconcatun  42087  clsk1independent  42797  ovnval  45257  sprval  46147  nnsum3primes4  46456  nnsum3primesprm  46458  nnsum3primesgbe  46460  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  zlidlring  46826  uzlidlring  46827  lcoop  47092  ldepsnlinc  47189  nnpw2p  47272  lines  47417  iscnrm3r  47581