Theorem sbcie 3771

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 3769	. 2 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ 𝜓))
4	1, 3	ax-mp 5	1 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  Vcvv 3432  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731

This theorem is referenced by:  sbc2ie  3805  csbie  3873  rexopabb  5477  reuop  6251  tfinds2  7811  soseq  8106  findcard2  9096  ac6sfi  9191  ac6num  10399  fpwwe  10567  nn1suc  12194  wrdind  14682  cjth  15063  fprodser  15912  prmind2  16652  joinlem  18345  meetlem  18359  mndind  18794  isghm  19188  isghmOLD  19189  islmod  20861  islindf  21794  fgcl  23868  cfinfil  23883  csdfil  23884  supfil  23885  fin1aufil  23922  quotval  26283  dfconngr1  30283  isconngr  30284  isconngr1  30285  wrdt2ind  33039  bnj62  34910  bnj610  34937  bnj976  34967  bnj106  35057  bnj125  35061  bnj154  35067  bnj155  35068  bnj526  35077  bnj540  35081  bnj591  35100  bnj609  35106  bnj893  35117  bnj1417  35230  poimirlem27  38021  sdclem2  38116  fdc  38119  fdc1  38120  lshpkrlem3  39611  hdmap1fval  42295  hdmapfval  42326  sn-isghm  43130  rabren3dioph  43267  2nn0ind  43397  zindbi  43398  onfrALTlem5  44993  onfrALTlem5VD  45335  reupr  48004