Theorem rexeqbidv 3344

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-rex 3068

This theorem is referenced by:  frd  5644  supeq123d  9487  fpwwe2lem12  10679  vdwpc  17013  ramval  17041  mreexexlemd  17688  iscat  17716  iscatd  17717  catidex  17718  gsumval2a  18710  ismnddef  18761  mndpropd  18784  isgrp  18969  isgrpd2e  18985  cayleyth  19447  psgnfval  19532  iscyg  19911  ltbval  22078  opsrval  22081  scmatval  22525  pmatcollpw3fi1lem2  22808  pmatcollpw3fi1  22809  neiptopnei  23155  is1stc  23464  2ndc1stc  23474  2ndcsep  23482  islly  23491  isnlly  23492  ucnval  24301  imasdsf1olem  24398  met2ndc  24551  evthicc  25507  elmade2  27921  addsval  28009  mulsval  28149  istrkgb  28477  istrkge  28479  istrkgld  28481  legval  28606  ishpg  28781  iscgra  28831  isinag  28860  isleag  28869  nbgrval  29367  nb3grprlem2  29412  1loopgrvd0  29536  erclwwlkeq  30046  eucrctshift  30271  isplig  30504  nmoofval  30790  erlval  33244  idomsubr  33290  elrsp  33379  1arithidom  33544  dfufd2lem  33556  constrsuc  33742  reprsuc  34608  istrkg2d  34659  iscvm  35243  cvmlift2lem13  35299  br8  35735  br6  35736  br4  35737  brsegle  36089  hilbert1.1  36135  pibp21  37397  poimirlem26  37632  poimirlem28  37634  poimirlem29  37635  cover2g  37702  isexid  37833  isrngo  37883  isrngod  37884  isgrpda  37941  lshpset  38959  cvrfval  39249  isatl  39280  ishlat1  39333  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  lcfl7N  41483  lcfrlem8  41531  lcfrlem9  41532  lcf1o  41533  hvmapffval  41740  hvmapfval  41741  hvmapval  41742  prjspval  42589  mzpcompact2lem  42738  eldioph  42745  aomclem8  43049  tfsconcatun  43326  clsk1independent  44035  ovnval  46496  sprval  47403  nnsum3primes4  47712  nnsum3primesprm  47714  nnsum3primesgbe  47716  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  clnbgrval  47746  zlidlring  48077  uzlidlring  48078  lcoop  48256  ldepsnlinc  48353  nnpw2p  48435  lines  48580  iscnrm3r  48744