Theorem raleqbidv 2685

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

Hypotheses

Ref	Expression
raleqbidv.1	|- ( ph -> A = B )
raleqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
raleqbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 |- ( ph -> A = B )
2	1	raleqdv 2679	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2477	. 2 |- ( ph -> ( A. x e. B ps <-> A. x e. B ch ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   A.wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  rspc2vd  3127  ofrfval  6093  fmpox  6203  tfrlemi1  6335  supeq123d  6992  cvg1nlemcau  10995  cvg1nlemres  10996  cau3lem  11125  fsum2dlemstep  11444  fisumcom2  11448  fprod2dlemstep  11632  fprodcom2fi  11636  pcfac  12350  ptex  12718  prdsex  12723  ismgm  12781  mgm1  12794  grpidvalg  12797  issgrp  12814  sgrp1  12821  ismnddef  12824  ismndd  12843  mndpropd  12846  mnd1  12852  ismhm  12858  isgrp  12888  grppropd  12898  isgrpd2e  12901  grp1  12981  isnsg  13067  nmznsg  13078  cmnpropd  13103  iscmnd  13106  dfur2g  13150  issrg  13153  issrgid  13169  isring  13188  iscrng2  13203  ringideu  13205  isringid  13213  ringpropd  13222  ring1  13241  oppr0g  13256  oppr1g  13257  islring  13338  islmod  13386  islmodd  13388  lmodprop2d  13443  lsssetm  13449  istopg  13538  restbasg  13707  cnfval  13733  cnpfval  13734  txbas  13797  limccl  14167  sscoll2  14779