Theorem raleqbidv 2709

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 2699	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2497	. 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 1364   A.wral 2475

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  rspc2vd  3153  ofrfval  6148  fmpox  6262  tfrlemi1  6394  supeq123d  7061  cvg1nlemcau  11154  cvg1nlemres  11155  cau3lem  11284  fsum2dlemstep  11604  fisumcom2  11608  fprod2dlemstep  11792  fprodcom2fi  11796  pcfac  12532  ptex  12954  prdsex  12959  prdsval  12963  ismgm  13047  mgm1  13060  grpidvalg  13063  gsumress  13085  issgrp  13093  sgrp1  13101  sgrppropd  13103  ismnddef  13106  ismndd  13125  mndpropd  13128  mnd1  13134  ismhm  13140  mhmex  13141  resmhm  13166  isgrp  13185  grppropd  13196  isgrpd2e  13199  grp1  13285  isnsg  13379  nmznsg  13390  isghm  13420  cmnpropd  13472  iscmnd  13475  isrng  13537  rngpropd  13558  dfur2g  13565  issrg  13568  issrgid  13584  isring  13603  iscrng2  13618  ringideu  13620  isringid  13628  ringpropd  13641  ring1  13662  oppr0g  13684  oppr1g  13685  isrhm2d  13768  rhmopp  13779  islring  13795  rrgval  13865  isdomn  13872  opprdomnbg  13877  islmod  13894  islmodd  13896  lmodprop2d  13951  lsssetm  13959  islidlm  14082  rnglidlmmgm  14099  rnglidlmsgrp  14100  istopg  14282  restbasg  14451  cnfval  14477  cnpfval  14478  txbas  14541  limccl  14942  sscoll2  15681