Theorem rexeqbidv 3338

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2146  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-rex 3090

This theorem is used by:  frd  5611  supeq123d  9452  fpwwe2lem12  10737  vdwpc  17170  ramval  17198  mreexexlemd  17830  iscat  17858  iscatd  17859  catidex  17860  idressidex  18873  gsumval2a  18886  ismnddef  18937  mndpropd  18963  isgrp  19162  isgrpd2e  19178  cayleyth  19641  psgnfval  19726  iscyg  20105  ltbval  22364  opsrval  22367  scmatval  22831  pmatcollpw3fi1lem2  23117  pmatcollpw3fi1  23118  neiptopnei  23462  is1stc  23771  2ndc1stc  23781  2ndcsep  23790  islly  23799  isnlly  23800  ucnval  24607  imasdsf1olem  24704  met2ndc  24854  evthicc  25792  elmade2  28256  addsval  28360  mulsval  28507  istrkgb  28929  istrkge  28931  istrkgld  28933  legval  29059  ishpg  29249  plngval  29267  lnssplng  29282  iscgra  29328  isinag  29369  isleag  29378  cgrabasimass  29390  nbgrval  29929  nb3grprlem2  29974  1loopgrvd0  30097  erclwwlkeq  30621  eucrctshift  30856  isplig  31090  nmoofval  31376  erlval  33872  idomsubr  33924  elrsp  33980  1arithidom  34122  dfufd2lem  34134  fldextrspunlsp  34359  extdgfialglem1  34377  constrsuc  34423  reprsuc  35297  istrkg2d  35348  iscvm  36145  cvmlift2lem13  36201  br8  36648  br6  36649  br4  36650  brsegle  37000  hilbert1.1  37046  pibp21  38478  poimirlem26  38704  poimirlem28  38706  poimirlem29  38707  cover2g  38790  isexid  38921  isrngo  38971  isrngod  38972  isgrpda  39029  lshpset  40175  cvrfval  40465  isatl  40496  ishlat1  40549  llnset  40702  lplnset  40726  lvolset  40769  lineset  40935  lcfl7N  42698  lcfrlem8  42746  lcfrlem9  42747  lcf1o  42748  hvmapffval  42955  hvmapfval  42956  hvmapval  42957  prjspval  43771  mzpcompact2lem  43902  eldioph  43909  aomclem8  44203  tfsconcatun  44479  clsk1independent  45186  ovnval  47690  sprval  48700  nnsum3primes4  49025  nnsum3primesprm  49027  nnsum3primesgbe  49029  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  clnbgrval  49059  gpg3kgrtriex  49326  grlimedgnedg  49368  zlidlring  49470  uzlidlring  49471  lcoop  49662  ldepsnlinc  49759  nnpw2p  49837  lines  49983  iscnrm3r  50201