Theorem rexeqbidv 3343

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-rex 3071

This theorem is referenced by:  frd  5635  supeq123d  9447  fpwwe2lem12  10639  vdwpc  16915  ramval  16943  mreexexlemd  17590  iscat  17618  iscatd  17619  catidex  17620  gsumval2a  18606  ismnddef  18629  mndpropd  18652  isgrp  18827  isgrpd2e  18843  cayleyth  19285  psgnfval  19370  iscyg  19749  ltbval  21604  opsrval  21607  scmatval  22013  pmatcollpw3fi1lem2  22296  pmatcollpw3fi1  22297  neiptopnei  22643  is1stc  22952  2ndc1stc  22962  2ndcsep  22970  islly  22979  isnlly  22980  ucnval  23789  imasdsf1olem  23886  met2ndc  24039  evthicc  24983  elmade2  27371  addsval  27455  mulsval  27575  istrkgb  27744  istrkge  27746  istrkgld  27748  legval  27873  ishpg  28048  iscgra  28098  isinag  28127  isleag  28136  nbgrval  28631  nb3grprlem2  28676  1loopgrvd0  28799  erclwwlkeq  29309  eucrctshift  29534  isplig  29767  nmoofval  30053  elrsp  32531  reprsuc  33696  istrkg2d  33747  iscvm  34319  cvmlift2lem13  34375  br8  34795  br6  34796  br4  34797  brsegle  35149  hilbert1.1  35195  pibp21  36382  poimirlem26  36600  poimirlem28  36602  poimirlem29  36603  cover2g  36670  isexid  36801  isrngo  36851  isrngod  36852  isgrpda  36909  lshpset  37934  cvrfval  38224  isatl  38255  ishlat1  38308  llnset  38462  lplnset  38486  lvolset  38529  lineset  38695  lcfl7N  40458  lcfrlem8  40506  lcfrlem9  40507  lcf1o  40508  hvmapffval  40715  hvmapfval  40716  hvmapval  40717  prjspval  41427  mzpcompact2lem  41571  eldioph  41578  aomclem8  41885  tfsconcatun  42169  clsk1independent  42879  ovnval  45336  sprval  46226  nnsum3primes4  46535  nnsum3primesprm  46537  nnsum3primesgbe  46539  wtgoldbnnsum4prm  46549  bgoldbnnsum3prm  46551  zlidlring  46905  uzlidlring  46906  lcoop  47170  ldepsnlinc  47267  nnpw2p  47350  lines  47495  iscnrm3r  47659