Theorem rexeqbidv 3314

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-rex 3064

This theorem is referenced by:  frd  5575  supeq123d  9353  fpwwe2lem12  10556  vdwpc  16942  ramval  16970  mreexexlemd  17601  iscat  17629  iscatd  17630  catidex  17631  gsumval2a  18644  ismnddef  18695  mndpropd  18718  isgrp  18906  isgrpd2e  18922  cayleyth  19381  psgnfval  19466  iscyg  19845  ltbval  22019  opsrval  22022  scmatval  22487  pmatcollpw3fi1lem2  22770  pmatcollpw3fi1  22771  neiptopnei  23115  is1stc  23424  2ndc1stc  23434  2ndcsep  23442  islly  23451  isnlly  23452  ucnval  24259  imasdsf1olem  24356  met2ndc  24506  evthicc  25444  elmade2  27868  addsval  27972  mulsval  28119  istrkgb  28541  istrkge  28543  istrkgld  28545  legval  28670  ishpg  28845  iscgra  28895  isinag  28924  isleag  28933  nbgrval  29423  nb3grprlem2  29468  1loopgrvd0  29591  erclwwlkeq  30106  eucrctshift  30331  isplig  30565  nmoofval  30851  erlval  33339  idomsubr  33393  elrsp  33455  1arithidom  33620  dfufd2lem  33632  fldextrspunlsp  33858  extdgfialglem1  33876  constrsuc  33922  reprsuc  34799  istrkg2d  34850  iscvm  35487  cvmlift2lem13  35543  br8  35984  br6  35985  br4  35986  brsegle  36336  hilbert1.1  36382  pibp21  37777  poimirlem26  38013  poimirlem28  38015  poimirlem29  38016  cover2g  38083  isexid  38214  isrngo  38264  isrngod  38265  isgrpda  38322  lshpset  39470  cvrfval  39760  isatl  39791  ishlat1  39844  llnset  39997  lplnset  40021  lvolset  40064  lineset  40230  lcfl7N  41993  lcfrlem8  42041  lcfrlem9  42042  lcf1o  42043  hvmapffval  42250  hvmapfval  42251  hvmapval  42252  prjspval  43053  mzpcompact2lem  43200  eldioph  43207  aomclem8  43506  tfsconcatun  43782  clsk1independent  44490  ovnval  46984  sprval  47954  nnsum3primes4  48279  nnsum3primesprm  48281  nnsum3primesgbe  48283  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  clnbgrval  48313  gpg3kgrtriex  48580  grlimedgnedg  48622  zlidlring  48725  uzlidlring  48726  lcoop  48902  ldepsnlinc  48999  nnpw2p  49077  lines  49222  iscnrm3r  49438