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  6243  fmpox  6364  tfrlemi1  6497  supeq123d  7189  acneq  7416  cvg1nlemcau  11544  cvg1nlemres  11545  cau3lem  11674  fsum2dlemstep  11994  fisumcom2  11998  fprod2dlemstep  12182  fprodcom2fi  12186  pcfac  12922  ptex  13346  prdsex  13351  prdsval  13355  ismgm  13439  mgm1  13452  grpidvalg  13455  gsumress  13477  issgrp  13485  sgrp1  13493  sgrppropd  13495  ismnddef  13500  ismndd  13519  mndpropd  13522  mnd1  13537  ismhm  13543  mhmex  13544  resmhm  13569  isgrp  13588  grppropd  13599  isgrpd2e  13602  grp1  13688  isnsg  13788  nmznsg  13799  isghm  13829  cmnpropd  13881  iscmnd  13884  isrng  13946  rngpropd  13967  dfur2g  13974  issrg  13977  issrgid  13993  isring  14012  iscrng2  14027  ringideu  14029  isringid  14037  ringpropd  14050  ring1  14071  oppr0g  14093  oppr1g  14094  isrhm2d  14178  rhmopp  14189  islring  14205  rrgval  14275  isdomn  14282  opprdomnbg  14287  islmod  14304  islmodd  14306  lmodprop2d  14361  lsssetm  14369  islidlm  14492  rnglidlmmgm  14509  rnglidlmsgrp  14510  mplvalcoe  14703  istopg  14722  restbasg  14891  cnfval  14917  cnpfval  14918  txbas  14981  limccl  15382  iswlk  16173  isclwwlk  16244  sscoll2  16583