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 3451  [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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740

This theorem is used by:  sbc2ie  3814  csbie  3882  rexopabb  5502  reuop  6295  tfinds2  7873  soseq  8169  findcard2  9173  ac6sfi  9268  ac6num  10550  fpwwe  10724  nn1suc  12350  wrdind  14864  cjth  15263  fprodser  16109  prmind2  16853  joinlem  18548  meetlem  18562  mndind  19017  isghm  19423  islmod  21132  islindf  22111  fgcl  24190  cfinfil  24205  csdfil  24206  supfil  24207  fin1aufil  24244  quotval  26606  dfconngr1  30782  isconngr  30783  isconngr1  30784  wrdt2ind  33509  bnj62  35344  bnj610  35371  bnj976  35401  bnj106  35491  bnj125  35495  bnj154  35501  bnj155  35502  bnj526  35511  bnj540  35515  bnj591  35534  bnj609  35540  bnj893  35551  bnj1417  35664  poimirlem27  38545  sdclem2  38656  fdc  38659  fdc1  38660  lshpkrlem3  40149  hdmap1fval  42833  hdmapfval  42864  sn-isghm  43664  rabren3dioph  43801  2nn0ind  43931  zindbi  43932  onfrALTlem5  45510  onfrALTlem5VD  45852  reupr  48573