Theorem rexeqbidv 3130

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)

Hypotheses

Ref	Expression
raleqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
raleqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexeqbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rexeqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	rexeqdv 3122	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rexbidv 3034	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 267	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902

This theorem is referenced by:  supeq123d  8239  fpwwe2lem13  9343  hashge2el2difr  13118  vdwpc  15522  ramval  15550  mreexexlemd  16127  iscat  16156  iscatd  16157  catidex  16158  gsumval2a  17102  ismnddef  17119  mndpropd  17139  isgrp  17251  isgrpd2e  17264  cayleyth  17658  psgnfval  17743  iscyg  18104  ltbval  19292  opsrval  19295  scmatval  20129  pmatcollpw3fi1lem2  20411  pmatcollpw3fi1  20412  neiptopnei  20746  is1stc  21054  2ndc1stc  21064  2ndcsep  21072  islly  21081  isnlly  21082  ucnval  21891  imasdsf1olem  21988  met2ndc  22138  evthicc  23035  istrkgld  25158  legval  25279  ishpg  25451  iscgra  25501  isinag  25529  isleag  25533  nb3graprlem2  25981  erclwwlkeq  26339  2wlksot  26394  2spthsot  26395  isplig  26720  nmoofval  27001  istrkg2d  29997  iscvm  30495  cvmlift2lem13  30551  br8  30899  br6  30900  br4  30901  brsegle  31385  hilbert1.1  31431  poimirlem26  32605  poimirlem28  32607  poimirlem29  32608  cover2g  32679  isexid  32816  isrngo  32866  isrngod  32867  isgrpda  32924  lshpset  33283  cvrfval  33573  isatl  33604  ishlat1  33657  llnset  33809  lplnset  33833  lvolset  33876  lineset  34042  lcfl7N  35808  lcfrlem8  35856  lcfrlem9  35857  lcf1o  35858  hvmapffval  36065  hvmapfval  36066  hvmapval  36067  mzpcompact2lem  36332  eldioph  36339  aomclem8  36649  clsk1independent  37364  ovnval  39431  nnsum3primes4  40204  nnsum3primesprm  40206  nnsum3primesgbe  40208  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  nbgrval  40560  nb3grprlem2  40609  1loopgrvd0  40719  erclwwlkseq  41239  eucrctshift  41411  zlidlring  41718  uzlidlring  41719  lcoop  41994  ldepsnlinc  42091  nnpw2p  42178