Theorem rexeqbidv 3320

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  frd  5595  supeq123d  9401  fpwwe2lem12  10595  vdwpc  16951  ramval  16979  mreexexlemd  17605  iscat  17633  iscatd  17634  catidex  17635  gsumval2a  18612  ismnddef  18663  mndpropd  18686  isgrp  18871  isgrpd2e  18887  cayleyth  19345  psgnfval  19430  iscyg  19809  ltbval  21950  opsrval  21953  scmatval  22391  pmatcollpw3fi1lem2  22674  pmatcollpw3fi1  22675  neiptopnei  23019  is1stc  23328  2ndc1stc  23338  2ndcsep  23346  islly  23355  isnlly  23356  ucnval  24164  imasdsf1olem  24261  met2ndc  24411  evthicc  25360  elmade2  27780  addsval  27869  mulsval  28012  istrkgb  28382  istrkge  28384  istrkgld  28386  legval  28511  ishpg  28686  iscgra  28736  isinag  28765  isleag  28774  nbgrval  29263  nb3grprlem2  29308  1loopgrvd0  29432  erclwwlkeq  29947  eucrctshift  30172  isplig  30405  nmoofval  30691  erlval  33209  idomsubr  33259  elrsp  33343  1arithidom  33508  dfufd2lem  33520  fldextrspunlsp  33669  constrsuc  33728  reprsuc  34606  istrkg2d  34657  iscvm  35246  cvmlift2lem13  35302  br8  35743  br6  35744  br4  35745  brsegle  36096  hilbert1.1  36142  pibp21  37403  poimirlem26  37640  poimirlem28  37642  poimirlem29  37643  cover2g  37710  isexid  37841  isrngo  37891  isrngod  37892  isgrpda  37949  lshpset  38971  cvrfval  39261  isatl  39292  ishlat1  39345  llnset  39499  lplnset  39523  lvolset  39566  lineset  39732  lcfl7N  41495  lcfrlem8  41543  lcfrlem9  41544  lcf1o  41545  hvmapffval  41752  hvmapfval  41753  hvmapval  41754  prjspval  42591  mzpcompact2lem  42739  eldioph  42746  aomclem8  43050  tfsconcatun  43326  clsk1independent  44035  ovnval  46539  sprval  47477  nnsum3primes4  47786  nnsum3primesprm  47788  nnsum3primesgbe  47790  wtgoldbnnsum4prm  47800  bgoldbnnsum3prm  47802  clnbgrval  47820  gpg3kgrtriex  48077  zlidlring  48219  uzlidlring  48220  lcoop  48397  ldepsnlinc  48494  nnpw2p  48572  lines  48717  iscnrm3r  48933