Theorem raleqbidv 2757

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525

This theorem is referenced by:  rspc2vd  3207  ofrfval  6275  fmpox  6396  tfrlemi1  6563  supeq123d  7282  acneq  7509  cvg1nlemcau  11669  cvg1nlemres  11670  cau3lem  11799  fsum2dlemstep  12120  fisumcom2  12124  fprod2dlemstep  12308  fprodcom2fi  12312  pcfac  13048  ptex  13477  prdsex  13482  prdsval  13486  ismgm  13570  mgm1  13583  grpidvalg  13586  gsumress  13608  issgrp  13616  sgrp1  13624  sgrppropd  13626  ismnddef  13631  ismndd  13650  mndpropd  13653  mnd1  13668  ismhm  13674  mhmex  13675  resmhm  13700  isgrp  13719  grppropd  13730  isgrpd2e  13733  grp1  13819  isnsg  13919  nmznsg  13930  isghm  13960  cmnpropd  14012  iscmnd  14015  isrng  14078  rngpropd  14099  dfur2g  14106  issrg  14109  issrgid  14125  isring  14144  iscrng2  14159  ringideu  14161  isringid  14169  ringpropd  14182  ring1  14203  oppr0g  14225  oppr1g  14226  isrhm2d  14310  rhmopp  14321  islring  14337  rrgval  14407  isdomn  14415  opprdomnbg  14420  islmod  14439  islmodd  14441  lmodprop2d  14496  lsssetm  14504  islidlm  14627  rnglidlmmgm  14644  rnglidlmsgrp  14645  mplvalcoe  14845  istopg  14864  restbasg  15033  cnfval  15059  cnpfval  15060  txbas  15123  limccl  15524  iswlk  16318  isclwwlk  16389  sscoll2  16758