Theorem rexeqbidv 3337

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-rex 3087

This theorem is referenced by:  frd  5604  supeq123d  9396  fpwwe2lem12  10600  vdwpc  17016  ramval  17044  mreexexlemd  17676  iscat  17704  iscatd  17705  catidex  17706  gsumval2a  18719  ismnddef  18770  mndpropd  18793  isgrp  18981  isgrpd2e  18997  cayleyth  19455  psgnfval  19540  iscyg  19919  ltbval  22096  opsrval  22099  scmatval  22564  pmatcollpw3fi1lem2  22847  pmatcollpw3fi1  22848  neiptopnei  23192  is1stc  23501  2ndc1stc  23511  2ndcsep  23519  islly  23528  isnlly  23529  ucnval  24336  imasdsf1olem  24433  met2ndc  24583  evthicc  25521  elmade2  27951  addsval  28055  mulsval  28202  istrkgb  28624  istrkge  28626  istrkgld  28628  legval  28753  ishpg  28932  plngval  28984  lnssplng  28999  iscgra  29003  isinag  29032  isleag  29041  nbgrval  29537  nb3grprlem2  29582  1loopgrvd0  29705  erclwwlkeq  30220  eucrctshift  30445  isplig  30679  nmoofval  30965  erlval  33439  idomsubr  33496  elrsp  33558  1arithidom  33733  dfufd2lem  33745  fldextrspunlsp  33971  extdgfialglem1  33989  constrsuc  34035  reprsuc  34909  istrkg2d  34960  iscvm  35609  cvmlift2lem13  35665  br8  36106  br6  36107  br4  36108  brsegle  36458  hilbert1.1  36504  pibp21  37909  poimirlem26  38145  poimirlem28  38147  poimirlem29  38148  cover2g  38215  isexid  38346  isrngo  38396  isrngod  38397  isgrpda  38454  lshpset  39602  cvrfval  39892  isatl  39923  ishlat1  39976  llnset  40129  lplnset  40153  lvolset  40196  lineset  40362  lcfl7N  42125  lcfrlem8  42173  lcfrlem9  42174  lcf1o  42175  hvmapffval  42382  hvmapfval  42383  hvmapval  42384  prjspval  43185  mzpcompact2lem  43332  eldioph  43339  aomclem8  43638  tfsconcatun  43914  clsk1independent  44622  ovnval  47115  sprval  48085  nnsum3primes4  48410  nnsum3primesprm  48412  nnsum3primesgbe  48414  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  clnbgrval  48444  gpg3kgrtriex  48711  grlimedgnedg  48753  zlidlring  48856  uzlidlring  48857  lcoop  49033  ldepsnlinc  49130  nnpw2p  49208  lines  49353  iscnrm3r  49569