Theorem sbcieg 3311

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1454   e. wcel 1897   [.wsbc 3278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279

This theorem is referenced by:  sbcie  3313  ralsng  4017  rexsng  4018  rabsnif  4053  ralrnmpt  6053  fpwwe2lem3  9083  nn1suc  10657  mrcmndind  16661  fgcl  20941  cfinfil  20956  csdfil  20957  supfil  20958  fin1aufil  20995  ifeqeqx  28206  nn0min  28432  bnj1452  29909  cdlemk35s  34548  cdlemk39s  34550  cdlemk42  34552  2nn0ind  35837  zindbi  35838  trsbcVD  37313  onfrALTlem5VD  37321