Theorem hbcsb1 2021

Description: Bound-variable hypothesis builder for substitution into a class.

Hypotheses

Ref	Expression
hbcsb1.1	|- A e. V
hbcsb1.2	|- (y e. A -> A.x y e. A)

Assertion

Ref	Expression
hbcsb1	|- (y e. [_A / x]_B -> A.x y e. [_A / x]_B)

Distinct variable groups:   y,A   x,y

Proof of Theorem hbcsb1

Step	Hyp	Ref	Expression
1		hbcsb1.1	. 2 |- A e. V
2		hbcsb1.2	. . 3 |- (y e. A -> A.x y e. A)
3	2	hbcsb1g 2020	. 2 |- (A e. V -> (y e. [_A / x]_B -> A.x y e. [_A / x]_B))
4	1, 3	ax-mp 7	1 |- (y e. [_A / x]_B -> A.x y e. [_A / x]_B)

Syntax hints:   -> wi 3  A.wal 952   e. wcel 956  Vcvv 1807  [_csb 1997

This theorem is referenced by:  csbieb 2026  csbie2t 2029  uniiunlem 2128  sbcbrg 2657  csbima12g 3405  csbfv12g 3733  fvopab4gf 3772  fvopab4sf 3773  fvopabs 3783  fopabcos 3824  csboprg 3977  oprabval2gf 4017  foprab2 4109  csbnegg 5344  fsum1slem 6954  fsump1slem 6958  isumnn0nna 7151  infcvgaux1 7162  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag4 7204

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-10 964  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-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-sbc 1938  df-csb 1998

Copyright terms: Public domain