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  6267  tfrlemi1  6399  supeq123d  7066  acneq  7285  cvg1nlemcau  11166  cvg1nlemres  11167  cau3lem  11296  fsum2dlemstep  11616  fisumcom2  11620  fprod2dlemstep  11804  fprodcom2fi  11808  pcfac  12544  ptex  12966  prdsex  12971  prdsval  12975  ismgm  13059  mgm1  13072  grpidvalg  13075  gsumress  13097  issgrp  13105  sgrp1  13113  sgrppropd  13115  ismnddef  13120  ismndd  13139  mndpropd  13142  mnd1  13157  ismhm  13163  mhmex  13164  resmhm  13189  isgrp  13208  grppropd  13219  isgrpd2e  13222  grp1  13308  isnsg  13408  nmznsg  13419  isghm  13449  cmnpropd  13501  iscmnd  13504  isrng  13566  rngpropd  13587  dfur2g  13594  issrg  13597  issrgid  13613  isring  13632  iscrng2  13647  ringideu  13649  isringid  13657  ringpropd  13670  ring1  13691  oppr0g  13713  oppr1g  13714  isrhm2d  13797  rhmopp  13808  islring  13824  rrgval  13894  isdomn  13901  opprdomnbg  13906  islmod  13923  islmodd  13925  lmodprop2d  13980  lsssetm  13988  islidlm  14111  rnglidlmmgm  14128  rnglidlmsgrp  14129  istopg  14319  restbasg  14488  cnfval  14514  cnpfval  14515  txbas  14578  limccl  14979  sscoll2  15718