Theorem sbcg 3846

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

Assertion

Ref	Expression
sbcg	⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem sbcg

Step	Hyp	Ref	Expression
1		nfv 1911	. 2 ⊢ Ⅎ𝑥𝜑
2	1	sbcgf 3844	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2110  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  sbcabel  3860  2nreu  4392  csbuni  4859  csbxp  5644  sbcfung  6373  fmptsnd  6925  opsbc2ie  30233  f1od2  30451  bnj89  31986  bnj525  32004  bnj1128  32257  csbwrecsg  34602  csbrdgg  34604  csboprabg  34605  mptsnunlem  34613  topdifinffinlem  34622  relowlpssretop  34639  rdgeqoa  34645  csbfinxpg  34663  gm-sbtru  35378  sbfal  35379  cdlemk40  38047  cdlemkid3N  38063  cdlemkid4  38064  frege70  40272  frege77  40279  frege116  40318  frege118  40320  trsbc  40867  trsbcVD  41204  csbxpgVD  41221  csbunigVD  41225