Theorem sbcg 3355

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3353. (Contributed by Alan Sare, 10-Nov-2012.)

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem sbcg

Step	Hyp	Ref	Expression
1		nfv 1674	. 2 |- F/ x ph
2	1	sbcgf 3353	1 |- ( A e. V -> ( [. A / x ]. ph <-> ph ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1758   [.wsbc 3281

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 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3067  df-sbc 3282

This theorem is referenced by:  sbcabel  3370  csbuni  4214  csbunigOLD  4215  csbxp  5013  csbxpgOLD  5014  sbcfung  5536  f1od2  26155  sbtru  29046  sbfal  29047  fmptsnd  30857  trsbc  31544  csbxpgVD  31927  csbunigVD  31931  bnj89  32007  bnj525  32027  bnj1128  32278  cdlemk40  34864  cdlemkid3N  34880  cdlemkid4  34881