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  17581  iscat  17609  iscatd  17610  catidex  17611  gsumval2a  18588  ismnddef  18639  mndpropd  18662  isgrp  18847  isgrpd2e  18863  cayleyth  19321  psgnfval  19406  iscyg  19785  ltbval  21926  opsrval  21929  scmatval  22367  pmatcollpw3fi1lem2  22650  pmatcollpw3fi1  22651  neiptopnei  22995  is1stc  23304  2ndc1stc  23314  2ndcsep  23322  islly  23331  isnlly  23332  ucnval  24140  imasdsf1olem  24237  met2ndc  24387  evthicc  25336  elmade2  27756  addsval  27845  mulsval  27988  istrkgb  28358  istrkge  28360  istrkgld  28362  legval  28487  ishpg  28662  iscgra  28712  isinag  28741  isleag  28750  nbgrval  29239  nb3grprlem2  29284  1loopgrvd0  29408  erclwwlkeq  29920  eucrctshift  30145  isplig  30378  nmoofval  30664  erlval  33182  idomsubr  33232  elrsp  33316  1arithidom  33481  dfufd2lem  33493  fldextrspunlsp  33642  constrsuc  33701  reprsuc  34579  istrkg2d  34630  iscvm  35219  cvmlift2lem13  35275  br8  35716  br6  35717  br4  35718  brsegle  36069  hilbert1.1  36115  pibp21  37376  poimirlem26  37613  poimirlem28  37615  poimirlem29  37616  cover2g  37683  isexid  37814  isrngo  37864  isrngod  37865  isgrpda  37922  lshpset  38944  cvrfval  39234  isatl  39265  ishlat1  39318  llnset  39472  lplnset  39496  lvolset  39539  lineset  39705  lcfl7N  41468  lcfrlem8  41516  lcfrlem9  41517  lcf1o  41518  hvmapffval  41725  hvmapfval  41726  hvmapval  41727  prjspval  42564  mzpcompact2lem  42712  eldioph  42719  aomclem8  43023  tfsconcatun  43299  clsk1independent  44008  ovnval  46512  sprval  47453  nnsum3primes4  47762  nnsum3primesprm  47764  nnsum3primesgbe  47766  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  clnbgrval  47796  gpg3kgrtriex  48053  zlidlring  48195  uzlidlring  48196  lcoop  48373  ldepsnlinc  48470  nnpw2p  48548  lines  48693  iscnrm3r  48909