Theorem sbcg 3503

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

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 1990  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-sbc 3436

This theorem is referenced by:  sbcabel  3517  csbuni  4466  csbxp  5200  sbcfung  5912  fmptsnd  6435  f1od2  29499  bnj89  30787  bnj525  30807  bnj1128  31058  csbwrecsg  33173  csbrdgg  33175  csboprabg  33176  mptsnunlem  33185  topdifinffinlem  33195  relowlpssretop  33212  rdgeqoa  33218  csbfinxpg  33225  sbtru  33908  sbfal  33909  cdlemk40  36205  cdlemkid3N  36221  cdlemkid4  36222  frege70  38227  frege77  38234  frege116  38273  frege118  38275  trsbc  38750  csbunigOLD  39051  csbxpgOLD  39053  csbxpgVD  39130  csbunigVD  39134