Theorem rexeqbidv 3402

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-rex 3144

This theorem is referenced by:  rexeqbi1dv  3404  supeq123d  8914  fpwwe2lem13  10064  vdwpc  16316  ramval  16344  mreexexlemd  16915  iscat  16943  iscatd  16944  catidex  16945  gsumval2a  17895  ismnddef  17913  mndpropd  17936  isgrp  18109  isgrpd2e  18122  cayleyth  18543  psgnfval  18628  iscyg  18998  ltbval  20252  opsrval  20255  scmatval  21113  pmatcollpw3fi1lem2  21395  pmatcollpw3fi1  21396  neiptopnei  21740  is1stc  22049  2ndc1stc  22059  2ndcsep  22067  islly  22076  isnlly  22077  ucnval  22886  imasdsf1olem  22983  met2ndc  23133  evthicc  24060  istrkgld  26245  legval  26370  ishpg  26545  iscgra  26595  isinag  26624  isleag  26633  nbgrval  27118  nb3grprlem2  27163  1loopgrvd0  27286  erclwwlkeq  27796  eucrctshift  28022  isplig  28253  nmoofval  28539  reprsuc  31886  istrkg2d  31937  iscvm  32506  cvmlift2lem13  32562  br8  32992  br6  32993  br4  32994  brsegle  33569  hilbert1.1  33615  pibp21  34699  poimirlem26  34933  poimirlem28  34935  poimirlem29  34936  cover2g  35005  isexid  35140  isrngo  35190  isrngod  35191  isgrpda  35248  lshpset  36129  cvrfval  36419  isatl  36450  ishlat1  36503  llnset  36656  lplnset  36680  lvolset  36723  lineset  36889  lcfl7N  38652  lcfrlem8  38700  lcfrlem9  38701  lcf1o  38702  hvmapffval  38909  hvmapfval  38910  hvmapval  38911  prjspval  39273  mzpcompact2lem  39368  eldioph  39375  aomclem8  39681  clsk1independent  40416  ovnval  42843  sprval  43661  nnsum3primes4  43973  nnsum3primesprm  43975  nnsum3primesgbe  43977  wtgoldbnnsum4prm  43987  bgoldbnnsum3prm  43989  zlidlring  44219  uzlidlring  44220  lcoop  44486  ldepsnlinc  44583  nnpw2p  44666  lines  44738