Theorem ra4csbela 2038

Description: Special case related to ra4sbc 1993. (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 1993	. . 3 |- (A e. B -> (A.x e. B C e. D -> [A / x]C e. D))
2		sbcel1g 2009	. . 3 |- (A e. B -> ([A / x]C e. D <-> [_A / x]_C e. D))
3	1, 2	sylibd 202	. 2 |- (A e. B -> (A.x e. B C e. D -> [_A / x]_C e. D))
4	3	imp 350	1 |- ((A e. B /\ A.x e. B C e. D) -> [_A / x]_C e. D)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956  [wsbc 1168  A.wral 1642  [_csb 1997

This theorem is referenced by:  fsumcllem 6960  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsummulc1 6979  fsumcmp 6986  fsumabs 6989  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag4 7204  fsumcnlem 7939

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ral 1646  df-v 1808  df-sbc 1938  df-csb 1998

Copyright terms: Public domain