Theorem rexeqbidv 3312

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-rex 3062

This theorem is referenced by:  frd  5588  supeq123d  9363  fpwwe2lem12  10565  vdwpc  16951  ramval  16979  mreexexlemd  17610  iscat  17638  iscatd  17639  catidex  17640  gsumval2a  18653  ismnddef  18704  mndpropd  18727  isgrp  18915  isgrpd2e  18931  cayleyth  19390  psgnfval  19475  iscyg  19854  ltbval  22021  opsrval  22024  scmatval  22469  pmatcollpw3fi1lem2  22752  pmatcollpw3fi1  22753  neiptopnei  23097  is1stc  23406  2ndc1stc  23416  2ndcsep  23424  islly  23433  isnlly  23434  ucnval  24241  imasdsf1olem  24338  met2ndc  24488  evthicc  25426  elmade2  27850  addsval  27954  mulsval  28101  istrkgb  28523  istrkge  28525  istrkgld  28527  legval  28652  ishpg  28827  iscgra  28877  isinag  28906  isleag  28915  nbgrval  29405  nb3grprlem2  29450  1loopgrvd0  29573  erclwwlkeq  30088  eucrctshift  30313  isplig  30547  nmoofval  30833  erlval  33319  idomsubr  33370  elrsp  33432  1arithidom  33597  dfufd2lem  33609  fldextrspunlsp  33818  extdgfialglem1  33836  constrsuc  33882  reprsuc  34759  istrkg2d  34810  iscvm  35441  cvmlift2lem13  35497  br8  35938  br6  35939  br4  35940  brsegle  36290  hilbert1.1  36336  pibp21  37731  poimirlem26  37967  poimirlem28  37969  poimirlem29  37970  cover2g  38037  isexid  38168  isrngo  38218  isrngod  38219  isgrpda  38276  lshpset  39424  cvrfval  39714  isatl  39745  ishlat1  39798  llnset  39951  lplnset  39975  lvolset  40018  lineset  40184  lcfl7N  41947  lcfrlem8  41995  lcfrlem9  41996  lcf1o  41997  hvmapffval  42204  hvmapfval  42205  hvmapval  42206  prjspval  43036  mzpcompact2lem  43183  eldioph  43190  aomclem8  43489  tfsconcatun  43765  clsk1independent  44473  ovnval  46969  sprval  47939  nnsum3primes4  48264  nnsum3primesprm  48266  nnsum3primesgbe  48268  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  clnbgrval  48298  gpg3kgrtriex  48565  grlimedgnedg  48607  zlidlring  48710  uzlidlring  48711  lcoop  48887  ldepsnlinc  48984  nnpw2p  49062  lines  49207  iscnrm3r  49423