Theorem ra4csbela 2045

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

Assertion

Ref	Expression
ra4csbela	⊢ ((A ∈ B ⋀ ∀x ∈ B C ∈ D) → [A / x]C ∈ D)

Distinct variable groups:   x,B   x,D

Proof of Theorem ra4csbela

Step	Hyp	Ref	Expression
1		ra4sbc 2000	. . 3 ⊢ (A ∈ B → (∀x ∈ B C ∈ D → [A / x]C ∈ D))
2		sbcel1g 2016	. . 3 ⊢ (A ∈ B → ([A / x]C ∈ D ↔ [A / x]C ∈ D))
3	1, 2	sylibd 202	. 2 ⊢ (A ∈ B → (∀x ∈ B C ∈ D → [A / x]C ∈ D))
4	3	imp 350	1 ⊢ ((A ∈ B ⋀ ∀x ∈ B C ∈ D) → [A / x]C ∈ D)

Syntax hints:   → wi 3   ⋀ wa 223   ∈ wcel 960  [wsbc 1172  ∀wral 1648  [csb 2004

This theorem is referenced by:  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumcom 7028  fsumrev 7029  fsummulc1 7033  fsumcmp 7040  fsumabs 7043  fsum0diaglem2 7257  fsum0diag2 7259  fsum0diag4 7261  fsumcnlem 7986

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-sbc 1945  df-csb 2005

Copyright terms: Public domain