Theorem rexeqbidv 3335

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-rex 3087

This theorem is used by:  frd  5612  supeq123d  9421  fpwwe2lem12  10652  vdwpc  17073  ramval  17101  mreexexlemd  17733  iscat  17761  iscatd  17762  catidex  17763  idressidex  18775  gsumval2a  18788  ismnddef  18839  mndpropd  18865  isgrp  19064  isgrpd2e  19080  cayleyth  19543  psgnfval  19628  iscyg  20007  ltbval  22260  opsrval  22263  scmatval  22727  pmatcollpw3fi1lem2  23013  pmatcollpw3fi1  23014  neiptopnei  23358  is1stc  23667  2ndc1stc  23677  2ndcsep  23686  islly  23695  isnlly  23696  ucnval  24503  imasdsf1olem  24600  met2ndc  24750  evthicc  25688  elmade2  28124  addsval  28228  mulsval  28375  istrkgb  28797  istrkge  28799  istrkgld  28801  legval  28927  ishpg  29117  plngval  29135  lnssplng  29150  iscgra  29196  isinag  29237  isleag  29246  cgrabasimass  29258  nbgrval  29797  nb3grprlem2  29842  1loopgrvd0  29965  erclwwlkeq  30489  eucrctshift  30724  isplig  30958  nmoofval  31244  erlval  33699  idomsubr  33751  elrsp  33807  1arithidom  33948  dfufd2lem  33960  fldextrspunlsp  34185  extdgfialglem1  34203  constrsuc  34249  reprsuc  35124  istrkg2d  35175  iscvm  35839  cvmlift2lem13  35895  br8  36336  br6  36337  br4  36338  brsegle  36689  hilbert1.1  36735  pibp21  38170  poimirlem26  38396  poimirlem28  38398  poimirlem29  38399  cover2g  38467  isexid  38598  isrngo  38648  isrngod  38649  isgrpda  38706  lshpset  39852  cvrfval  40142  isatl  40173  ishlat1  40226  llnset  40379  lplnset  40403  lvolset  40446  lineset  40612  lcfl7N  42375  lcfrlem8  42423  lcfrlem9  42424  lcf1o  42425  hvmapffval  42632  hvmapfval  42633  hvmapval  42634  prjspval  43450  mzpcompact2lem  43597  eldioph  43604  aomclem8  43903  tfsconcatun  44179  clsk1independent  44887  ovnval  47370  sprval  48380  nnsum3primes4  48705  nnsum3primesprm  48707  nnsum3primesgbe  48709  wtgoldbnnsum4prm  48719  bgoldbnnsum3prm  48721  clnbgrval  48739  gpg3kgrtriex  49006  grlimedgnedg  49048  zlidlring  49150  uzlidlring  49151  lcoop  49342  ldepsnlinc  49439  nnpw2p  49517  lines  49662  iscnrm3r  49875