Theorem sbcie 3754

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  Vcvv 3422  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbc2ie  3795  csbie  3864  rexopabb  5434  reuop  6185  tfinds2  7685  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  ac6num  10166  fpwwe  10333  nn1suc  11925  wrdind  14363  cjth  14742  fprodser  15587  prmind2  16318  joinlem  18016  meetlem  18030  mndind  18381  isghm  18749  islmod  20042  islindf  20929  fgcl  22937  cfinfil  22952  csdfil  22953  supfil  22954  fin1aufil  22991  quotval  25357  dfconngr1  28453  isconngr  28454  isconngr1  28455  wrdt2ind  31127  bnj62  32599  bnj610  32627  bnj976  32657  bnj106  32748  bnj125  32752  bnj154  32758  bnj155  32759  bnj526  32768  bnj540  32772  bnj591  32791  bnj609  32797  bnj893  32808  bnj1417  32921  soseq  33730  poimirlem27  35731  sdclem2  35827  fdc  35830  fdc1  35831  lshpkrlem3  37053  hdmap1fval  39737  hdmapfval  39768  rabren3dioph  40553  2nn0ind  40683  zindbi  40684  onfrALTlem5  42051  onfrALTlem5VD  42394  reupr  44862