Theorem rexeqbidv 3355

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∃wrex 3107

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-rex 3112

This theorem is referenced by:  rexeqbi1dv  3357  supeq123d  8898  fpwwe2lem13  10053  vdwpc  16306  ramval  16334  mreexexlemd  16907  iscat  16935  iscatd  16936  catidex  16937  gsumval2a  17887  ismnddef  17905  mndpropd  17928  isgrp  18101  isgrpd2e  18114  cayleyth  18535  psgnfval  18620  iscyg  18991  ltbval  20711  opsrval  20714  scmatval  21109  pmatcollpw3fi1lem2  21392  pmatcollpw3fi1  21393  neiptopnei  21737  is1stc  22046  2ndc1stc  22056  2ndcsep  22064  islly  22073  isnlly  22074  ucnval  22883  imasdsf1olem  22980  met2ndc  23130  evthicc  24063  istrkgld  26253  legval  26378  ishpg  26553  iscgra  26603  isinag  26632  isleag  26641  nbgrval  27126  nb3grprlem2  27171  1loopgrvd0  27294  erclwwlkeq  27803  eucrctshift  28028  isplig  28259  nmoofval  28545  elrsp  30989  reprsuc  31996  istrkg2d  32047  iscvm  32619  cvmlift2lem13  32675  br8  33105  br6  33106  br4  33107  brsegle  33682  hilbert1.1  33728  pibp21  34832  poimirlem26  35083  poimirlem28  35085  poimirlem29  35086  cover2g  35153  isexid  35285  isrngo  35335  isrngod  35336  isgrpda  35393  lshpset  36274  cvrfval  36564  isatl  36595  ishlat1  36648  llnset  36801  lplnset  36825  lvolset  36868  lineset  37034  lcfl7N  38797  lcfrlem8  38845  lcfrlem9  38846  lcf1o  38847  hvmapffval  39054  hvmapfval  39055  hvmapval  39056  prjspval  39597  mzpcompact2lem  39692  eldioph  39699  aomclem8  40005  clsk1independent  40749  ovnval  43180  sprval  43996  nnsum3primes4  44306  nnsum3primesprm  44308  nnsum3primesgbe  44310  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  zlidlring  44552  uzlidlring  44553  lcoop  44820  ldepsnlinc  44917  nnpw2p  45000  lines  45145