Theorem rexeqbidv 3327

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774  df-rex 3096

This theorem is referenced by:  rexeqbi1dv  3329  supeq123d  8644  fpwwe2lem13  9799  vdwpc  16088  ramval  16116  mreexexlemd  16690  iscat  16718  iscatd  16719  catidex  16720  gsumval2a  17665  ismnddef  17682  mndpropd  17702  isgrp  17815  isgrpd2e  17828  cayleyth  18218  psgnfval  18304  iscyg  18667  ltbval  19868  opsrval  19871  scmatval  20715  pmatcollpw3fi1lem2  20999  pmatcollpw3fi1  21000  neiptopnei  21344  is1stc  21653  2ndc1stc  21663  2ndcsep  21671  islly  21680  isnlly  21681  ucnval  22489  imasdsf1olem  22586  met2ndc  22736  evthicc  23663  istrkgld  25810  legval  25935  ishpg  26107  iscgra  26157  isinag  26187  isleag  26196  nbgrval  26683  nb3grprlem2  26729  1loopgrvd0  26852  erclwwlkeq  27407  eucrctshift  27647  isplig  27903  nmoofval  28189  reprsuc  31295  istrkg2d  31346  iscvm  31840  cvmlift2lem13  31896  br8  32240  br6  32241  br4  32242  brsegle  32804  hilbert1.1  32850  poimirlem26  34061  poimirlem28  34063  poimirlem29  34064  cover2g  34134  isexid  34270  isrngo  34320  isrngod  34321  isgrpda  34378  lshpset  35132  cvrfval  35422  isatl  35453  ishlat1  35506  llnset  35659  lplnset  35683  lvolset  35726  lineset  35892  lcfl7N  37655  lcfrlem8  37703  lcfrlem9  37704  lcf1o  37705  hvmapffval  37912  hvmapfval  37913  hvmapval  37914  prjspval  38204  mzpcompact2lem  38274  eldioph  38281  aomclem8  38590  clsk1independent  39300  ovnval  41682  sprval  42418  nnsum3primes4  42701  nnsum3primesprm  42703  nnsum3primesgbe  42705  wtgoldbnnsum4prm  42715  bgoldbnnsum3prm  42717  zlidlring  42943  uzlidlring  42944  lcoop  43215  ldepsnlinc  43312  nnpw2p  43395  lines  43467