Theorem rexeqbidv 3317

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-rex 3061

This theorem is referenced by:  frd  5581  supeq123d  9353  fpwwe2lem12  10553  vdwpc  16908  ramval  16936  mreexexlemd  17567  iscat  17595  iscatd  17596  catidex  17597  gsumval2a  18610  ismnddef  18661  mndpropd  18684  isgrp  18869  isgrpd2e  18885  cayleyth  19344  psgnfval  19429  iscyg  19808  ltbval  21998  opsrval  22001  scmatval  22448  pmatcollpw3fi1lem2  22731  pmatcollpw3fi1  22732  neiptopnei  23076  is1stc  23385  2ndc1stc  23395  2ndcsep  23403  islly  23412  isnlly  23413  ucnval  24220  imasdsf1olem  24317  met2ndc  24467  evthicc  25416  elmade2  27854  addsval  27958  mulsval  28105  istrkgb  28527  istrkge  28529  istrkgld  28531  legval  28656  ishpg  28831  iscgra  28881  isinag  28910  isleag  28919  nbgrval  29409  nb3grprlem2  29454  1loopgrvd0  29578  erclwwlkeq  30093  eucrctshift  30318  isplig  30551  nmoofval  30837  erlval  33340  idomsubr  33391  elrsp  33453  1arithidom  33618  dfufd2lem  33630  fldextrspunlsp  33831  extdgfialglem1  33849  constrsuc  33895  reprsuc  34772  istrkg2d  34823  iscvm  35453  cvmlift2lem13  35509  br8  35950  br6  35951  br4  35952  brsegle  36302  hilbert1.1  36348  pibp21  37620  poimirlem26  37847  poimirlem28  37849  poimirlem29  37850  cover2g  37917  isexid  38048  isrngo  38098  isrngod  38099  isgrpda  38156  lshpset  39238  cvrfval  39528  isatl  39559  ishlat1  39612  llnset  39765  lplnset  39789  lvolset  39832  lineset  39998  lcfl7N  41761  lcfrlem8  41809  lcfrlem9  41810  lcf1o  41811  hvmapffval  42018  hvmapfval  42019  hvmapval  42020  prjspval  42846  mzpcompact2lem  42993  eldioph  43000  aomclem8  43303  tfsconcatun  43579  clsk1independent  44287  ovnval  46785  sprval  47725  nnsum3primes4  48034  nnsum3primesprm  48036  nnsum3primesgbe  48038  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  clnbgrval  48068  gpg3kgrtriex  48335  grlimedgnedg  48377  zlidlring  48480  uzlidlring  48481  lcoop  48657  ldepsnlinc  48754  nnpw2p  48832  lines  48977  iscnrm3r  49193