Theorem rexeqbidv 3341

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720  df-clel 2806  df-rex 3068

This theorem is referenced by:  frd  5641  supeq123d  9481  fpwwe2lem12  10673  vdwpc  16956  ramval  16984  mreexexlemd  17631  iscat  17659  iscatd  17660  catidex  17661  gsumval2a  18652  ismnddef  18703  mndpropd  18726  isgrp  18903  isgrpd2e  18919  cayleyth  19377  psgnfval  19462  iscyg  19841  ltbval  21988  opsrval  21991  scmatval  22426  pmatcollpw3fi1lem2  22709  pmatcollpw3fi1  22710  neiptopnei  23056  is1stc  23365  2ndc1stc  23375  2ndcsep  23383  islly  23392  isnlly  23393  ucnval  24202  imasdsf1olem  24299  met2ndc  24452  evthicc  25408  elmade2  27815  addsval  27899  mulsval  28029  istrkgb  28279  istrkge  28281  istrkgld  28283  legval  28408  ishpg  28583  iscgra  28633  isinag  28662  isleag  28671  nbgrval  29169  nb3grprlem2  29214  1loopgrvd0  29338  erclwwlkeq  29848  eucrctshift  30073  isplig  30306  nmoofval  30592  erlval  32997  idomsubr  33020  elrsp  33109  reprsuc  34280  istrkg2d  34331  iscvm  34902  cvmlift2lem13  34958  br8  35383  br6  35384  br4  35385  brsegle  35737  hilbert1.1  35783  pibp21  36927  poimirlem26  37152  poimirlem28  37154  poimirlem29  37155  cover2g  37222  isexid  37353  isrngo  37403  isrngod  37404  isgrpda  37461  lshpset  38482  cvrfval  38772  isatl  38803  ishlat1  38856  llnset  39010  lplnset  39034  lvolset  39077  lineset  39243  lcfl7N  41006  lcfrlem8  41054  lcfrlem9  41055  lcf1o  41056  hvmapffval  41263  hvmapfval  41264  hvmapval  41265  prjspval  42058  mzpcompact2lem  42202  eldioph  42209  aomclem8  42516  tfsconcatun  42797  clsk1independent  43507  ovnval  45958  sprval  46848  nnsum3primes4  47157  nnsum3primesprm  47159  nnsum3primesgbe  47161  wtgoldbnnsum4prm  47171  bgoldbnnsum3prm  47173  clnbgrval  47191  zlidlring  47374  uzlidlring  47375  lcoop  47557  ldepsnlinc  47654  nnpw2p  47737  lines  47882  iscnrm3r  48045