Theorem rexeqbidv 3339

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-rex 3090

This theorem is referenced by:  frd  5618  supeq123d  9406  fpwwe2lem12  10622  vdwpc  17035  ramval  17063  mreexexlemd  17695  iscat  17723  iscatd  17724  catidex  17725  gsumval2a  18738  ismnddef  18789  mndpropd  18812  isgrp  19001  isgrpd2e  19017  cayleyth  19480  psgnfval  19565  iscyg  19944  ltbval  22194  opsrval  22197  scmatval  22661  pmatcollpw3fi1lem2  22944  pmatcollpw3fi1  22945  neiptopnei  23289  is1stc  23598  2ndc1stc  23608  2ndcsep  23616  islly  23625  isnlly  23626  ucnval  24433  imasdsf1olem  24530  met2ndc  24680  evthicc  25618  elmade2  28051  addsval  28155  mulsval  28302  istrkgb  28724  istrkge  28726  istrkgld  28728  legval  28853  ishpg  29041  plngval  29059  lnssplng  29074  iscgra  29120  isinag  29155  isleag  29164  nbgrval  29686  nb3grprlem2  29731  1loopgrvd0  29854  erclwwlkeq  30369  eucrctshift  30594  isplig  30828  nmoofval  31114  erlval  33578  idomsubr  33630  elrsp  33686  1arithidom  33827  dfufd2lem  33839  fldextrspunlsp  34064  extdgfialglem1  34082  constrsuc  34128  reprsuc  35002  istrkg2d  35053  iscvm  35751  cvmlift2lem13  35807  br8  36248  br6  36249  br4  36250  brsegle  36600  hilbert1.1  36646  pibp21  38061  poimirlem26  38297  poimirlem28  38299  poimirlem29  38300  cover2g  38367  isexid  38498  isrngo  38548  isrngod  38549  isgrpda  38606  lshpset  39752  cvrfval  40042  isatl  40073  ishlat1  40126  llnset  40279  lplnset  40303  lvolset  40346  lineset  40512  lcfl7N  42275  lcfrlem8  42323  lcfrlem9  42324  lcf1o  42325  hvmapffval  42532  hvmapfval  42533  hvmapval  42534  prjspval  43335  mzpcompact2lem  43482  eldioph  43489  aomclem8  43788  tfsconcatun  44064  clsk1independent  44772  ovnval  47255  sprval  48228  nnsum3primes4  48553  nnsum3primesprm  48555  nnsum3primesgbe  48557  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  clnbgrval  48587  gpg3kgrtriex  48854  grlimedgnedg  48896  zlidlring  48999  uzlidlring  49000  lcoop  49191  ldepsnlinc  49288  nnpw2p  49366  lines  49511  iscnrm3r  49726