Theorem raleqbidv 2744

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  rspc2vd  3193  ofrfval  6233  fmpox  6352  tfrlemi1  6484  supeq123d  7169  acneq  7395  cvg1nlemcau  11511  cvg1nlemres  11512  cau3lem  11641  fsum2dlemstep  11961  fisumcom2  11965  fprod2dlemstep  12149  fprodcom2fi  12153  pcfac  12889  ptex  13313  prdsex  13318  prdsval  13322  ismgm  13406  mgm1  13419  grpidvalg  13422  gsumress  13444  issgrp  13452  sgrp1  13460  sgrppropd  13462  ismnddef  13467  ismndd  13486  mndpropd  13489  mnd1  13504  ismhm  13510  mhmex  13511  resmhm  13536  isgrp  13555  grppropd  13566  isgrpd2e  13569  grp1  13655  isnsg  13755  nmznsg  13766  isghm  13796  cmnpropd  13848  iscmnd  13851  isrng  13913  rngpropd  13934  dfur2g  13941  issrg  13944  issrgid  13960  isring  13979  iscrng2  13994  ringideu  13996  isringid  14004  ringpropd  14017  ring1  14038  oppr0g  14060  oppr1g  14061  isrhm2d  14145  rhmopp  14156  islring  14172  rrgval  14242  isdomn  14249  opprdomnbg  14254  islmod  14271  islmodd  14273  lmodprop2d  14328  lsssetm  14336  islidlm  14459  rnglidlmmgm  14476  rnglidlmsgrp  14477  mplvalcoe  14670  istopg  14689  restbasg  14858  cnfval  14884  cnpfval  14885  txbas  14948  limccl  15349  iswlk  16069  isclwwlk  16137  sscoll2  16434