Theorem sbcieg 3369

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)

Hypothesis

Ref	Expression
sbcieg.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
sbcieg	|- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Distinct variable groups:   x, A   ps, x

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem sbcieg

Step	Hyp	Ref	Expression
1		nfv 1683	. 2 |- F/ x ps
2		sbcieg.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	sbciegf 3368	1 |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   [.wsbc 3336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3120  df-sbc 3337

This theorem is referenced by:  sbcie  3371  ralsng  4068  rexsng  4069  rabsnif  4102  ralrnmpt  6041  fpwwe2lem3  9023  nn1suc  10569  mrcmndind  15869  fgcl  20247  cfinfil  20262  csdfil  20263  supfil  20264  fin1aufil  20301  ifeqeqx  27242  nn0min  27435  2nn0ind  30809  zindbi  30810  trsbcVD  33158  onfrALTlem5VD  33166  bnj1452  33588  cdlemk35s  36134  cdlemk39s  36136  cdlemk42  36138