Theorem sbcieg 3327

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   e. wcel 1758   [.wsbc 3294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080  df-sbc 3295

This theorem is referenced by:  sbcie  3329  ralsng  4023  rexsng  4024  rabsnif  4055  ralrnmpt  5964  fpwwe2lem3  8915  nn1suc  10458  mrcmndind  15617  fgcl  19593  cfinfil  19608  csdfil  19609  supfil  19610  fin1aufil  19647  ifeqeqx  26081  nn0min  26262  2nn0ind  29457  zindbi  29458  trsbcVD  31968  onfrALTlem5VD  31976  bnj1452  32398  cdlemk35s  34944  cdlemk39s  34946  cdlemk42  34948