Theorem rexeqbidv 3341

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-rex 3092

This theorem is used by:  frd  5620  supeq123d  9417  fpwwe2lem12  10642  vdwpc  17062  ramval  17090  mreexexlemd  17722  iscat  17750  iscatd  17751  catidex  17752  idressidex  18764  gsumval2a  18775  ismnddef  18826  mndpropd  18852  isgrp  19050  isgrpd2e  19066  cayleyth  19529  psgnfval  19614  iscyg  19993  ltbval  22244  opsrval  22247  scmatval  22711  pmatcollpw3fi1lem2  22994  pmatcollpw3fi1  22995  neiptopnei  23339  is1stc  23648  2ndc1stc  23658  2ndcsep  23667  islly  23676  isnlly  23677  ucnval  24484  imasdsf1olem  24581  met2ndc  24731  evthicc  25669  elmade2  28102  addsval  28206  mulsval  28353  istrkgb  28775  istrkge  28777  istrkgld  28779  legval  28904  ishpg  29092  plngval  29110  lnssplng  29125  iscgra  29171  isinag  29210  isleag  29219  nbgrval  29744  nb3grprlem2  29789  1loopgrvd0  29912  erclwwlkeq  30436  eucrctshift  30665  isplig  30899  nmoofval  31185  erlval  33642  idomsubr  33694  elrsp  33750  1arithidom  33891  dfufd2lem  33903  fldextrspunlsp  34128  extdgfialglem1  34146  constrsuc  34192  reprsuc  35067  istrkg2d  35118  iscvm  35788  cvmlift2lem13  35844  br8  36285  br6  36286  br4  36287  brsegle  36637  hilbert1.1  36683  pibp21  38118  poimirlem26  38354  poimirlem28  38356  poimirlem29  38357  cover2g  38425  isexid  38556  isrngo  38606  isrngod  38607  isgrpda  38664  lshpset  39810  cvrfval  40100  isatl  40131  ishlat1  40184  llnset  40337  lplnset  40361  lvolset  40404  lineset  40570  lcfl7N  42333  lcfrlem8  42381  lcfrlem9  42382  lcf1o  42383  hvmapffval  42590  hvmapfval  42591  hvmapval  42592  prjspval  43393  mzpcompact2lem  43540  eldioph  43547  aomclem8  43846  tfsconcatun  44122  clsk1independent  44830  ovnval  47313  sprval  48286  nnsum3primes4  48611  nnsum3primesprm  48613  nnsum3primesgbe  48615  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  clnbgrval  48645  gpg3kgrtriex  48912  grlimedgnedg  48954  zlidlring  49056  uzlidlring  49057  lcoop  49248  ldepsnlinc  49345  nnpw2p  49423  lines  49568  iscnrm3r  49783