Theorem hbsbc1v 1995

Description: Bound-variable hypothesis builder for class substitution.

Hypothesis

Ref	Expression
hbsbcv.1	|- A e. V

Assertion

Ref	Expression
hbsbc1v	|- ([A / x]ph -> A.x[A / x]ph)

Distinct variable group:   x,A

Proof of Theorem hbsbc1v

Step	Hyp	Ref	Expression
1		ax-17 1007	. . 3 |- (y e. A -> A.x y e. A)
2	1	hbsbc1 1994	. 2 |- ((A e. V -> [A / x]ph) -> A.x(A e. V -> [A / x]ph))
3		hbsbcv.1	. . 3 |- A e. V
4	3	a1bi 195	. 2 |- ([A / x]ph <-> (A e. V -> [A / x]ph))
5	4	albii 1035	. 2 |- (A.x[A / x]ph <-> A.x(A e. V -> [A / x]ph))
6	2, 4, 5	3imtr4i 217	1 |- ([A / x]ph -> A.x[A / x]ph)

Syntax hints:   -> wi 3  A.wal 990   e. wcel 994  [wsbc 1207  Vcvv 1857

This theorem is referenced by:  tfindes 3215  findes 3248  dfopab2 4173  dfoprab3 4174  ac6sfilem1 4588  ac6sfilem3 4590  ac6sfi 4591  nn1suc 6084  uzindOLD 6379  nn0ind-raph 6385  uzind4s 6579  fzrevral 6650  subtr2 11396  cbvsbc 11398  ac6gf 11841  indexd 11846  sdclem2 11876  sdc 11877

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-sbc 1987

Copyright terms: Public domain