Theorem sbcg 3847

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3845. (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 1915	. 2 ⊢ Ⅎ𝑥𝜑
2	1	sbcgf 3845	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2114  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3773

This theorem is referenced by:  sbcabel  3861  2nreu  4393  csbuni  4867  csbxp  5650  sbcfung  6379  fmptsnd  6931  opsbc2ie  30239  f1od2  30457  bnj89  31991  bnj525  32009  bnj1128  32262  csbwrecsg  34611  csbrdgg  34613  csboprabg  34614  mptsnunlem  34622  topdifinffinlem  34631  relowlpssretop  34648  rdgeqoa  34654  csbfinxpg  34672  gm-sbtru  35399  sbfal  35400  cdlemk40  38068  cdlemkid3N  38084  cdlemkid4  38085  frege70  40299  frege77  40306  frege116  40345  frege118  40347  trsbc  40894  trsbcVD  41231  csbxpgVD  41248  csbunigVD  41252