Theorem raleqbidv 2747

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 2737	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2533	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ∀wral 2511

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516

This theorem is referenced by:  rspc2vd  3197  ofrfval  6253  fmpox  6374  tfrlemi1  6541  supeq123d  7250  acneq  7477  cvg1nlemcau  11624  cvg1nlemres  11625  cau3lem  11754  fsum2dlemstep  12075  fisumcom2  12079  fprod2dlemstep  12263  fprodcom2fi  12267  pcfac  13003  ptex  13427  prdsex  13432  prdsval  13436  ismgm  13520  mgm1  13533  grpidvalg  13536  gsumress  13558  issgrp  13566  sgrp1  13574  sgrppropd  13576  ismnddef  13581  ismndd  13600  mndpropd  13603  mnd1  13618  ismhm  13624  mhmex  13625  resmhm  13650  isgrp  13669  grppropd  13680  isgrpd2e  13683  grp1  13769  isnsg  13869  nmznsg  13880  isghm  13910  cmnpropd  13962  iscmnd  13965  isrng  14028  rngpropd  14049  dfur2g  14056  issrg  14059  issrgid  14075  isring  14094  iscrng2  14109  ringideu  14111  isringid  14119  ringpropd  14132  ring1  14153  oppr0g  14175  oppr1g  14176  isrhm2d  14260  rhmopp  14271  islring  14287  rrgval  14357  isdomn  14365  opprdomnbg  14370  islmod  14387  islmodd  14389  lmodprop2d  14444  lsssetm  14452  islidlm  14575  rnglidlmmgm  14592  rnglidlmsgrp  14593  mplvalcoe  14791  istopg  14810  restbasg  14979  cnfval  15005  cnpfval  15006  txbas  15069  limccl  15470  iswlk  16264  isclwwlk  16335  sscoll2  16704