Theorem rexeqbidv 3338

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172 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 631	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3225	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-rex 3071

This theorem is referenced by:  frd  5549  supeq123d  9218  fpwwe2lem12  10407  vdwpc  16690  ramval  16718  mreexexlemd  17362  iscat  17390  iscatd  17391  catidex  17392  gsumval2a  18378  ismnddef  18396  mndpropd  18419  isgrp  18592  isgrpd2e  18607  cayleyth  19032  psgnfval  19117  iscyg  19488  ltbval  21253  opsrval  21256  scmatval  21662  pmatcollpw3fi1lem2  21945  pmatcollpw3fi1  21946  neiptopnei  22292  is1stc  22601  2ndc1stc  22611  2ndcsep  22619  islly  22628  isnlly  22629  ucnval  23438  imasdsf1olem  23535  met2ndc  23688  evthicc  24632  istrkgld  26829  legval  26954  ishpg  27129  iscgra  27179  isinag  27208  isleag  27217  nbgrval  27712  nb3grprlem2  27757  1loopgrvd0  27880  erclwwlkeq  28391  eucrctshift  28616  isplig  28847  nmoofval  29133  elrsp  31578  reprsuc  32604  istrkg2d  32655  iscvm  33230  cvmlift2lem13  33286  br8  33732  br6  33733  br4  33734  elmade2  34061  addsval  34135  brsegle  34419  hilbert1.1  34465  pibp21  35595  poimirlem26  35812  poimirlem28  35814  poimirlem29  35815  cover2g  35882  isexid  36014  isrngo  36064  isrngod  36065  isgrpda  36122  lshpset  36999  cvrfval  37289  isatl  37320  ishlat1  37373  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  lcfl7N  39522  lcfrlem8  39570  lcfrlem9  39571  lcf1o  39572  hvmapffval  39779  hvmapfval  39780  hvmapval  39781  prjspval  40449  mzpcompact2lem  40580  eldioph  40587  aomclem8  40893  clsk1independent  41663  ovnval  44086  sprval  44942  nnsum3primes4  45251  nnsum3primesprm  45253  nnsum3primesgbe  45255  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  zlidlring  45497  uzlidlring  45498  lcoop  45763  ldepsnlinc  45860  nnpw2p  45943  lines  46088  iscnrm3r  46253