Theorem rexeqbidv 3355

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, 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 2830	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	anbi12d 631	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3181	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-rex 3077

This theorem is referenced by:  frd  5656  supeq123d  9519  fpwwe2lem12  10711  vdwpc  17027  ramval  17055  mreexexlemd  17702  iscat  17730  iscatd  17731  catidex  17732  gsumval2a  18723  ismnddef  18774  mndpropd  18797  isgrp  18979  isgrpd2e  18995  cayleyth  19457  psgnfval  19542  iscyg  19921  ltbval  22084  opsrval  22087  scmatval  22531  pmatcollpw3fi1lem2  22814  pmatcollpw3fi1  22815  neiptopnei  23161  is1stc  23470  2ndc1stc  23480  2ndcsep  23488  islly  23497  isnlly  23498  ucnval  24307  imasdsf1olem  24404  met2ndc  24557  evthicc  25513  elmade2  27925  addsval  28013  mulsval  28153  istrkgb  28481  istrkge  28483  istrkgld  28485  legval  28610  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  nbgrval  29371  nb3grprlem2  29416  1loopgrvd0  29540  erclwwlkeq  30050  eucrctshift  30275  isplig  30508  nmoofval  30794  erlval  33230  idomsubr  33276  elrsp  33365  1arithidom  33530  dfufd2lem  33542  constrsuc  33728  reprsuc  34592  istrkg2d  34643  iscvm  35227  cvmlift2lem13  35283  br8  35718  br6  35719  br4  35720  brsegle  36072  hilbert1.1  36118  pibp21  37381  poimirlem26  37606  poimirlem28  37608  poimirlem29  37609  cover2g  37676  isexid  37807  isrngo  37857  isrngod  37858  isgrpda  37915  lshpset  38934  cvrfval  39224  isatl  39255  ishlat1  39308  llnset  39462  lplnset  39486  lvolset  39529  lineset  39695  lcfl7N  41458  lcfrlem8  41506  lcfrlem9  41507  lcf1o  41508  hvmapffval  41715  hvmapfval  41716  hvmapval  41717  prjspval  42558  mzpcompact2lem  42707  eldioph  42714  aomclem8  43018  tfsconcatun  43299  clsk1independent  44008  ovnval  46462  sprval  47353  nnsum3primes4  47662  nnsum3primesprm  47664  nnsum3primesgbe  47666  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  clnbgrval  47696  zlidlring  47957  uzlidlring  47958  lcoop  48140  ldepsnlinc  48237  nnpw2p  48320  lines  48465  iscnrm3r  48628