Theorem sbcieg 3346

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1383   e. wcel 1804   [.wsbc 3313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-sbc 3314

This theorem is referenced by:  sbcie  3348  ralsng  4049  rexsng  4050  rabsnif  4084  ralrnmpt  6025  fpwwe2lem3  9014  nn1suc  10563  mrcmndind  15871  fgcl  20252  cfinfil  20267  csdfil  20268  supfil  20269  fin1aufil  20306  ifeqeqx  27291  nn0min  27484  2nn0ind  30856  zindbi  30857  trsbcVD  33405  onfrALTlem5VD  33413  bnj1452  33836  cdlemk35s  36397  cdlemk39s  36399  cdlemk42  36401