Theorem sbcg 3390

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3388. (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 1712	. 2 |- F/ x ph
2	1	sbcgf 3388	1 |- ( A e. V -> ( [. A / x ]. ph <-> ph ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1823   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-sbc 3325

This theorem is referenced by:  sbcabel  3402  csbuni  4263  csbxp  5070  sbcfung  5593  fmptsnd  6069  f1od2  27781  sbtru  30751  sbfal  30752  trsbc  33720  csbunigOLD  34035  csbxpgOLD  34037  csbxpgVD  34114  csbunigVD  34118  bnj89  34194  bnj525  34214  bnj1128  34466  cdlemk40  37059  cdlemkid3N  37075  cdlemkid4  37076  frege70  38434  frege77  38441  frege116  38480  frege118  38482