Theorem rexeqbidv 3347

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-rex 3071

This theorem is referenced by:  frd  5641  supeq123d  9490  fpwwe2lem12  10682  vdwpc  17018  ramval  17046  mreexexlemd  17687  iscat  17715  iscatd  17716  catidex  17717  gsumval2a  18698  ismnddef  18749  mndpropd  18772  isgrp  18957  isgrpd2e  18973  cayleyth  19433  psgnfval  19518  iscyg  19897  ltbval  22061  opsrval  22064  scmatval  22510  pmatcollpw3fi1lem2  22793  pmatcollpw3fi1  22794  neiptopnei  23140  is1stc  23449  2ndc1stc  23459  2ndcsep  23467  islly  23476  isnlly  23477  ucnval  24286  imasdsf1olem  24383  met2ndc  24536  evthicc  25494  elmade2  27907  addsval  27995  mulsval  28135  istrkgb  28463  istrkge  28465  istrkgld  28467  legval  28592  ishpg  28767  iscgra  28817  isinag  28846  isleag  28855  nbgrval  29353  nb3grprlem2  29398  1loopgrvd0  29522  erclwwlkeq  30037  eucrctshift  30262  isplig  30495  nmoofval  30781  erlval  33262  idomsubr  33311  elrsp  33400  1arithidom  33565  dfufd2lem  33577  fldextrspunlsp  33724  constrsuc  33779  reprsuc  34630  istrkg2d  34681  iscvm  35264  cvmlift2lem13  35320  br8  35756  br6  35757  br4  35758  brsegle  36109  hilbert1.1  36155  pibp21  37416  poimirlem26  37653  poimirlem28  37655  poimirlem29  37656  cover2g  37723  isexid  37854  isrngo  37904  isrngod  37905  isgrpda  37962  lshpset  38979  cvrfval  39269  isatl  39300  ishlat1  39353  llnset  39507  lplnset  39531  lvolset  39574  lineset  39740  lcfl7N  41503  lcfrlem8  41551  lcfrlem9  41552  lcf1o  41553  hvmapffval  41760  hvmapfval  41761  hvmapval  41762  prjspval  42613  mzpcompact2lem  42762  eldioph  42769  aomclem8  43073  tfsconcatun  43350  clsk1independent  44059  ovnval  46556  sprval  47466  nnsum3primes4  47775  nnsum3primesprm  47777  nnsum3primesgbe  47779  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  clnbgrval  47809  gpg3kgrtriex  48045  zlidlring  48150  uzlidlring  48151  lcoop  48328  ldepsnlinc  48425  nnpw2p  48507  lines  48652  iscnrm3r  48845