Theorem rexeqbidv 3336

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 2847	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	anbi12d 644	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒)))
5	4	rexbidv2 3183	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-rex 3088

This theorem is used by:  frd  5608  supeq123d  9442  fpwwe2lem12  10727  vdwpc  17158  ramval  17186  mreexexlemd  17818  iscat  17846  iscatd  17847  catidex  17848  idressidex  18861  gsumval2a  18874  ismnddef  18925  mndpropd  18951  isgrp  19150  isgrpd2e  19166  cayleyth  19629  psgnfval  19714  iscyg  20093  ltbval  22352  opsrval  22355  scmatval  22819  pmatcollpw3fi1lem2  23105  pmatcollpw3fi1  23106  neiptopnei  23450  is1stc  23759  2ndc1stc  23769  2ndcsep  23778  islly  23787  isnlly  23788  ucnval  24595  imasdsf1olem  24692  met2ndc  24842  evthicc  25780  elmade2  28244  addsval  28348  mulsval  28495  istrkgb  28917  istrkge  28919  istrkgld  28921  legval  29047  ishpg  29237  plngval  29255  lnssplng  29270  iscgra  29316  isinag  29357  isleag  29366  cgrabasimass  29378  nbgrval  29917  nb3grprlem2  29962  1loopgrvd0  30085  erclwwlkeq  30609  eucrctshift  30844  isplig  31078  nmoofval  31364  erlval  33819  idomsubr  33871  elrsp  33927  1arithidom  34069  dfufd2lem  34081  fldextrspunlsp  34306  extdgfialglem1  34324  constrsuc  34370  reprsuc  35244  istrkg2d  35295  iscvm  36024  cvmlift2lem13  36080  br8  36521  br6  36522  br4  36523  brsegle  36873  hilbert1.1  36919  pibp21  38338  poimirlem26  38564  poimirlem28  38566  poimirlem29  38567  cover2g  38650  isexid  38781  isrngo  38831  isrngod  38832  isgrpda  38889  lshpset  40035  cvrfval  40325  isatl  40356  ishlat1  40409  llnset  40562  lplnset  40586  lvolset  40629  lineset  40795  lcfl7N  42558  lcfrlem8  42606  lcfrlem9  42607  lcf1o  42608  hvmapffval  42815  hvmapfval  42816  hvmapval  42817  prjspval  43631  mzpcompact2lem  43761  eldioph  43768  aomclem8  44062  tfsconcatun  44338  clsk1independent  45045  ovnval  47550  sprval  48560  nnsum3primes4  48885  nnsum3primesprm  48887  nnsum3primesgbe  48889  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  clnbgrval  48919  gpg3kgrtriex  49186  grlimedgnedg  49228  zlidlring  49330  uzlidlring  49331  lcoop  49522  ldepsnlinc  49619  nnpw2p  49697  lines  49842  iscnrm3r  50055