Theorem sbcie 3780

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  Vcvv 3450  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3740

This theorem is used by:  sbc2ie  3814  csbie  3882  rexopabb  5506  reuop  6291  tfinds2  7860  soseq  8157  findcard2  9159  ac6sfi  9254  ac6num  10481  fpwwe  10655  nn1suc  12279  wrdind  14791  cjth  15190  fprodser  16036  prmind2  16775  joinlem  18469  meetlem  18483  mndind  18937  isghm  19343  islmod  21048  islindf  22025  fgcl  24104  cfinfil  24119  csdfil  24120  supfil  24121  fin1aufil  24158  quotval  26522  dfconngr1  30668  isconngr  30669  isconngr1  30670  wrdt2ind  33395  bnj62  35230  bnj610  35257  bnj976  35287  bnj106  35377  bnj125  35381  bnj154  35387  bnj155  35388  bnj526  35397  bnj540  35401  bnj591  35420  bnj609  35426  bnj893  35437  bnj1417  35550  poimirlem27  38396  sdclem2  38492  fdc  38495  fdc1  38496  lshpkrlem3  39985  hdmap1fval  42669  hdmapfval  42700  sn-isghm  43519  rabren3dioph  43656  2nn0ind  43786  zindbi  43787  onfrALTlem5  45365  onfrALTlem5VD  45707  reupr  48422