Theorem raleqbidv 2746

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

Hypotheses

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

Assertion

Ref	Expression
raleqbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

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

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

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	raleqdv 2736	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2532	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  rspc2vd  3196  ofrfval  6244  fmpox  6365  tfrlemi1  6498  supeq123d  7190  acneq  7417  cvg1nlemcau  11562  cvg1nlemres  11563  cau3lem  11692  fsum2dlemstep  12013  fisumcom2  12017  fprod2dlemstep  12201  fprodcom2fi  12205  pcfac  12941  ptex  13365  prdsex  13370  prdsval  13374  ismgm  13458  mgm1  13471  grpidvalg  13474  gsumress  13496  issgrp  13504  sgrp1  13512  sgrppropd  13514  ismnddef  13519  ismndd  13538  mndpropd  13541  mnd1  13556  ismhm  13562  mhmex  13563  resmhm  13588  isgrp  13607  grppropd  13618  isgrpd2e  13621  grp1  13707  isnsg  13807  nmznsg  13818  isghm  13848  cmnpropd  13900  iscmnd  13903  isrng  13966  rngpropd  13987  dfur2g  13994  issrg  13997  issrgid  14013  isring  14032  iscrng2  14047  ringideu  14049  isringid  14057  ringpropd  14070  ring1  14091  oppr0g  14113  oppr1g  14114  isrhm2d  14198  rhmopp  14209  islring  14225  rrgval  14295  isdomn  14302  opprdomnbg  14307  islmod  14324  islmodd  14326  lmodprop2d  14381  lsssetm  14389  islidlm  14512  rnglidlmmgm  14529  rnglidlmsgrp  14530  mplvalcoe  14723  istopg  14742  restbasg  14911  cnfval  14937  cnpfval  14938  txbas  15001  limccl  15402  iswlk  16193  isclwwlk  16264  sscoll2  16634