Theorem rexeqbidv 3319

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  frd  5589  supeq123d  9365  fpwwe2lem12  10565  vdwpc  16920  ramval  16948  mreexexlemd  17579  iscat  17607  iscatd  17608  catidex  17609  gsumval2a  18622  ismnddef  18673  mndpropd  18696  isgrp  18881  isgrpd2e  18897  cayleyth  19356  psgnfval  19441  iscyg  19820  ltbval  22010  opsrval  22013  scmatval  22460  pmatcollpw3fi1lem2  22743  pmatcollpw3fi1  22744  neiptopnei  23088  is1stc  23397  2ndc1stc  23407  2ndcsep  23415  islly  23424  isnlly  23425  ucnval  24232  imasdsf1olem  24329  met2ndc  24479  evthicc  25428  elmade2  27866  addsval  27970  mulsval  28117  istrkgb  28539  istrkge  28541  istrkgld  28543  legval  28668  ishpg  28843  iscgra  28893  isinag  28922  isleag  28931  nbgrval  29421  nb3grprlem2  29466  1loopgrvd0  29590  erclwwlkeq  30105  eucrctshift  30330  isplig  30564  nmoofval  30850  erlval  33352  idomsubr  33403  elrsp  33465  1arithidom  33630  dfufd2lem  33642  fldextrspunlsp  33852  extdgfialglem1  33870  constrsuc  33916  reprsuc  34793  istrkg2d  34844  iscvm  35475  cvmlift2lem13  35531  br8  35972  br6  35973  br4  35974  brsegle  36324  hilbert1.1  36370  pibp21  37670  poimirlem26  37897  poimirlem28  37899  poimirlem29  37900  cover2g  37967  isexid  38098  isrngo  38148  isrngod  38149  isgrpda  38206  lshpset  39354  cvrfval  39644  isatl  39675  ishlat1  39728  llnset  39881  lplnset  39905  lvolset  39948  lineset  40114  lcfl7N  41877  lcfrlem8  41925  lcfrlem9  41926  lcf1o  41927  hvmapffval  42134  hvmapfval  42135  hvmapval  42136  prjspval  42961  mzpcompact2lem  43108  eldioph  43115  aomclem8  43418  tfsconcatun  43694  clsk1independent  44402  ovnval  46899  sprval  47839  nnsum3primes4  48148  nnsum3primesprm  48150  nnsum3primesgbe  48152  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  clnbgrval  48182  gpg3kgrtriex  48449  grlimedgnedg  48491  zlidlring  48594  uzlidlring  48595  lcoop  48771  ldepsnlinc  48868  nnpw2p  48946  lines  49091  iscnrm3r  49307