Theorem sbcg 3470

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

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403

This theorem is referenced by:  sbcabel  3483  csbuni  4402  csbxp  5123  sbcfung  5827  fmptsnd  6340  f1od2  28887  bnj89  30041  bnj525  30061  bnj1128  30312  csbwrecsg  32349  csbrdgg  32351  csboprabg  32352  mptsnunlem  32361  topdifinffinlem  32371  relowlpssretop  32388  rdgeqoa  32394  csbfinxpg  32401  sbtru  33078  sbfal  33079  cdlemk40  35223  cdlemkid3N  35239  cdlemkid4  35240  frege70  37247  frege77  37254  frege116  37293  frege118  37295  trsbc  37771  csbunigOLD  38073  csbxpgOLD  38075  csbxpgVD  38152  csbunigVD  38156