Theorem raleqbidv 2698

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 2692	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2490	. 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 2468

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473

This theorem is referenced by:  rspc2vd  3140  ofrfval  6110  fmpox  6220  tfrlemi1  6352  supeq123d  7015  cvg1nlemcau  11020  cvg1nlemres  11021  cau3lem  11150  fsum2dlemstep  11469  fisumcom2  11473  fprod2dlemstep  11657  fprodcom2fi  11661  pcfac  12377  ptex  12762  prdsex  12767  ismgm  12826  mgm1  12839  grpidvalg  12842  issgrp  12859  sgrp1  12867  sgrppropd  12869  ismnddef  12872  ismndd  12891  mndpropd  12894  mnd1  12900  ismhm  12906  mhmex  12907  resmhm  12932  isgrp  12944  grppropd  12955  isgrpd2e  12958  grp1  13043  isnsg  13134  nmznsg  13145  isghm  13175  cmnpropd  13227  iscmnd  13230  isrng  13281  rngpropd  13302  dfur2g  13309  issrg  13312  issrgid  13328  isring  13347  iscrng2  13362  ringideu  13364  isringid  13372  ringpropd  13385  ring1  13404  oppr0g  13424  oppr1g  13425  isrhm2d  13508  rhmopp  13519  islring  13532  islmod  13600  islmodd  13602  lmodprop2d  13657  lsssetm  13665  islidlm  13788  rnglidlmmgm  13805  rnglidlmsgrp  13806  istopg  13936  restbasg  14105  cnfval  14131  cnpfval  14132  txbas  14195  limccl  14565  sscoll2  15177