Theorem rexeqbidv 3339

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-rex 3091

This theorem is used by:  frd  5615  supeq123d  9479  fpwwe2lem12  10766  vdwpc  17202  ramval  17230  mreexexlemd  17868  iscat  17896  iscatd  17897  catidex  17898  idressidex  18911  gsumval2a  18924  ismnddef  18975  mndpropd  19001  isgrp  19200  isgrpd2e  19216  cayleyth  19680  psgnfval  19765  iscyg  20144  ltbval  22407  opsrval  22410  scmatval  22874  pmatcollpw3fi1lem2  23160  pmatcollpw3fi1  23161  neiptopnei  23505  is1stc  23814  2ndc1stc  23824  2ndcsep  23833  islly  23842  isnlly  23843  ucnval  24650  imasdsf1olem  24747  met2ndc  24897  evthicc  25835  elmade2  28301  addsval  28405  mulsval  28552  istrkgb  28974  istrkge  28976  istrkgld  28978  legval  29104  ishpg  29294  plngval  29312  lnssplng  29327  iscgra  29373  isinag  29414  isleag  29423  cgrabasimass  29435  nbgrval  29974  nb3grprlem2  30019  1loopgrvd0  30142  erclwwlkeq  30666  eucrctshift  30901  isplig  31135  nmoofval  31421  erlval  33918  isedom  33953  idomsubr  33975  elrsp  34031  1arithidom  34173  dfufd2lem  34185  fldextrspunlsp  34417  extdgfialglem1  34435  constrsuc  34481  reprsuc  35355  istrkg2d  35406  iscvm  36232  cvmlift2lem13  36288  br8  36736  br6  36737  br4  36738  brsegle  37088  hilbert1.1  37134  pibp21  38606  poimirlem26  38832  poimirlem28  38834  poimirlem29  38835  cover2g  38918  isexid  39047  isrngo  39097  isrngod  39098  isgrpda  39155  lshpset  40301  cvrfval  40591  isatl  40622  ishlat1  40675  llnset  40828  lplnset  40852  lvolset  40895  lineset  41061  lcfl7N  42824  lcfrlem8  42872  lcfrlem9  42873  lcf1o  42874  hvmapffval  43081  hvmapfval  43082  hvmapval  43083  prjspval  43897  mzpcompact2lem  44028  eldioph  44035  aomclem8  44329  tfsconcatun  44600  clsk1independent  45307  ovnval  47824  sprval  48834  nnsum3primes4  49159  nnsum3primesprm  49161  nnsum3primesgbe  49163  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  clnbgrval  49193  gpg3kgrtriex  49460  grlimedgnedg  49502  zlidlring  49604  uzlidlring  49605  lcoop  49854  ldepsnlinc  49951  nnpw2p  50029  lines  50175  iscnrm3r  50393