Theorem rexeqbidv 3313

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  frd  5582  supeq123d  9357  fpwwe2lem12  10559  vdwpc  16945  ramval  16973  mreexexlemd  17604  iscat  17632  iscatd  17633  catidex  17634  gsumval2a  18647  ismnddef  18698  mndpropd  18721  isgrp  18909  isgrpd2e  18925  cayleyth  19384  psgnfval  19469  iscyg  19848  ltbval  22034  opsrval  22037  scmatval  22482  pmatcollpw3fi1lem2  22765  pmatcollpw3fi1  22766  neiptopnei  23110  is1stc  23419  2ndc1stc  23429  2ndcsep  23437  islly  23446  isnlly  23447  ucnval  24254  imasdsf1olem  24351  met2ndc  24501  evthicc  25439  elmade2  27867  addsval  27971  mulsval  28118  istrkgb  28540  istrkge  28542  istrkgld  28544  legval  28669  ishpg  28844  iscgra  28894  isinag  28923  isleag  28932  nbgrval  29422  nb3grprlem2  29467  1loopgrvd0  29591  erclwwlkeq  30106  eucrctshift  30331  isplig  30565  nmoofval  30851  erlval  33337  idomsubr  33388  elrsp  33450  1arithidom  33615  dfufd2lem  33627  fldextrspunlsp  33837  extdgfialglem1  33855  constrsuc  33901  reprsuc  34778  istrkg2d  34829  iscvm  35460  cvmlift2lem13  35516  br8  35957  br6  35958  br4  35959  brsegle  36309  hilbert1.1  36355  pibp21  37748  poimirlem26  37984  poimirlem28  37986  poimirlem29  37987  cover2g  38054  isexid  38185  isrngo  38235  isrngod  38236  isgrpda  38293  lshpset  39441  cvrfval  39731  isatl  39762  ishlat1  39815  llnset  39968  lplnset  39992  lvolset  40035  lineset  40201  lcfl7N  41964  lcfrlem8  42012  lcfrlem9  42013  lcf1o  42014  hvmapffval  42221  hvmapfval  42222  hvmapval  42223  prjspval  43053  mzpcompact2lem  43200  eldioph  43207  aomclem8  43510  tfsconcatun  43786  clsk1independent  44494  ovnval  46990  sprval  47954  nnsum3primes4  48279  nnsum3primesprm  48281  nnsum3primesgbe  48283  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  clnbgrval  48313  gpg3kgrtriex  48580  grlimedgnedg  48622  zlidlring  48725  uzlidlring  48726  lcoop  48902  ldepsnlinc  48999  nnpw2p  49077  lines  49222  iscnrm3r  49438