Theorem raleqbidv 2744

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 2734	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2530	. 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 1395   A.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  6227  fmpox  6346  tfrlemi1  6478  supeq123d  7158  acneq  7384  cvg1nlemcau  11495  cvg1nlemres  11496  cau3lem  11625  fsum2dlemstep  11945  fisumcom2  11949  fprod2dlemstep  12133  fprodcom2fi  12137  pcfac  12873  ptex  13297  prdsex  13302  prdsval  13306  ismgm  13390  mgm1  13403  grpidvalg  13406  gsumress  13428  issgrp  13436  sgrp1  13444  sgrppropd  13446  ismnddef  13451  ismndd  13470  mndpropd  13473  mnd1  13488  ismhm  13494  mhmex  13495  resmhm  13520  isgrp  13539  grppropd  13550  isgrpd2e  13553  grp1  13639  isnsg  13739  nmznsg  13750  isghm  13780  cmnpropd  13832  iscmnd  13835  isrng  13897  rngpropd  13918  dfur2g  13925  issrg  13928  issrgid  13944  isring  13963  iscrng2  13978  ringideu  13980  isringid  13988  ringpropd  14001  ring1  14022  oppr0g  14044  oppr1g  14045  isrhm2d  14129  rhmopp  14140  islring  14156  rrgval  14226  isdomn  14233  opprdomnbg  14238  islmod  14255  islmodd  14257  lmodprop2d  14312  lsssetm  14320  islidlm  14443  rnglidlmmgm  14460  rnglidlmsgrp  14461  mplvalcoe  14654  istopg  14673  restbasg  14842  cnfval  14868  cnpfval  14869  txbas  14932  limccl  15333  iswlk  16036  sscoll2  16351