Theorem rexeqbidv 3330

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  df-rex 3062

This theorem is referenced by:  frd  5615  supeq123d  9467  fpwwe2lem12  10661  vdwpc  17005  ramval  17033  mreexexlemd  17661  iscat  17689  iscatd  17690  catidex  17691  gsumval2a  18668  ismnddef  18719  mndpropd  18742  isgrp  18927  isgrpd2e  18943  cayleyth  19401  psgnfval  19486  iscyg  19865  ltbval  22006  opsrval  22009  scmatval  22447  pmatcollpw3fi1lem2  22730  pmatcollpw3fi1  22731  neiptopnei  23075  is1stc  23384  2ndc1stc  23394  2ndcsep  23402  islly  23411  isnlly  23412  ucnval  24220  imasdsf1olem  24317  met2ndc  24467  evthicc  25417  elmade2  27837  addsval  27926  mulsval  28069  istrkgb  28439  istrkge  28441  istrkgld  28443  legval  28568  ishpg  28743  iscgra  28793  isinag  28822  isleag  28831  nbgrval  29320  nb3grprlem2  29365  1loopgrvd0  29489  erclwwlkeq  30004  eucrctshift  30229  isplig  30462  nmoofval  30748  erlval  33258  idomsubr  33308  elrsp  33392  1arithidom  33557  dfufd2lem  33569  fldextrspunlsp  33720  constrsuc  33777  reprsuc  34652  istrkg2d  34703  iscvm  35286  cvmlift2lem13  35342  br8  35778  br6  35779  br4  35780  brsegle  36131  hilbert1.1  36177  pibp21  37438  poimirlem26  37675  poimirlem28  37677  poimirlem29  37678  cover2g  37745  isexid  37876  isrngo  37926  isrngod  37927  isgrpda  37984  lshpset  39001  cvrfval  39291  isatl  39322  ishlat1  39375  llnset  39529  lplnset  39553  lvolset  39596  lineset  39762  lcfl7N  41525  lcfrlem8  41573  lcfrlem9  41574  lcf1o  41575  hvmapffval  41782  hvmapfval  41783  hvmapval  41784  prjspval  42601  mzpcompact2lem  42749  eldioph  42756  aomclem8  43060  tfsconcatun  43336  clsk1independent  44045  ovnval  46550  sprval  47473  nnsum3primes4  47782  nnsum3primesprm  47784  nnsum3primesgbe  47786  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  clnbgrval  47816  gpg3kgrtriex  48071  zlidlring  48189  uzlidlring  48190  lcoop  48367  ldepsnlinc  48464  nnpw2p  48546  lines  48691  iscnrm3r  48902