Theorem sbcieg 3207

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 1672	. 2 |- F/ x ps
2		sbcieg.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	sbciegf 3206	1 |- ( A e. V -> ( [. A / x ]. ph <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1362   e. wcel 1755   [.wsbc 3175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-sbc 3176

This theorem is referenced by:  sbcie  3209  ralsng  3900  rexsng  3901  rabsnif  3932  ralrnmpt  5840  fpwwe2lem3  8788  nn1suc  10331  mrcmndind  15476  fgcl  19293  cfinfil  19308  csdfil  19309  supfil  19310  fin1aufil  19347  ifeqeqx  25726  nn0min  25913  2nn0ind  29131  zindbi  29132  trsbcVD  31315  onfrALTlem5VD  31323  bnj1452  31745  cdlemk35s  34154  cdlemk39s  34156  cdlemk42  34158