Theorem sbcie 3770

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)

Hypotheses

Ref	Expression
sbcie.1	⊢ 𝐴 ∈ V
sbcie.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
sbcie	⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbcie

Step	Hyp	Ref	Expression
1		sbcie.1	. 2 ⊢ 𝐴 ∈ V
2		sbcie.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	sbcieg 3768	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3429  [wsbc 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  sbc2ie  3804  csbie  3872  rexopabb  5483  reuop  6257  tfinds2  7815  soseq  8109  findcard2  9099  ac6sfi  9194  ac6num  10401  fpwwe  10569  nn1suc  12196  wrdind  14684  cjth  15065  fprodser  15914  prmind2  16654  joinlem  18347  meetlem  18361  mndind  18796  isghm  19190  isghmOLD  19191  islmod  20859  islindf  21792  fgcl  23843  cfinfil  23858  csdfil  23859  supfil  23860  fin1aufil  23897  quotval  26258  dfconngr1  30258  isconngr  30259  isconngr1  30260  wrdt2ind  33013  bnj62  34863  bnj610  34890  bnj976  34920  bnj106  35010  bnj125  35014  bnj154  35020  bnj155  35021  bnj526  35030  bnj540  35034  bnj591  35053  bnj609  35059  bnj893  35070  bnj1417  35183  poimirlem27  37968  sdclem2  38063  fdc  38066  fdc1  38067  lshpkrlem3  39558  hdmap1fval  42242  hdmapfval  42273  sn-isghm  43106  rabren3dioph  43243  2nn0ind  43373  zindbi  43374  onfrALTlem5  44969  onfrALTlem5VD  45311  reupr  47982