Theorem ra4csbela 2587

Description: Special case related to ra4sbc 2536. (The proof was shortened by Eric Schmidt, 17-Jan-2007.)

Assertion

Ref	Expression
ra4csbela	|- ((A e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)

Distinct variable groups:   x,B   x,D

Proof of Theorem ra4csbela

Step	Hyp	Ref	Expression
1		ra4sbc 2536	. . 3 |- (A e. B -> (A.x e. B C e. D -> [A / x]C e. D))
2		sbcel1g 2556	. . 3 |- (A e. B -> ([A / x]C e. D <-> [_A / x]_C e. D))
3	1, 2	sylibd 219	. 2 |- (A e. B -> (A.x e. B C e. D -> [_A / x]_C e. D))
4	3	imp 377	1 |- ((A e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  [wsbc 1534  A.wral 2105  [_csb 2540

This theorem is referenced by:  fsumcllem 8274  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumcom 8288  fsumrev 8289  fsummulc1 8293  fsumcmp 8300  fsumabs 8303  fsum0diaglem2 8519  fsum0diag2 8521  fsum0diag4 8523  fsumcnlem 9267  clfsebs 14707  fprodadd 14713  fprodneg 14741  fsumlt 15821

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-v 2294  df-sbc 2454  df-csb 2541

Copyright terms: Public domain