Theorem sbcie 3786

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  Vcvv 3455  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746

This theorem is referenced by:  sbc2ie  3820  csbie  3889  rexopabb  5514  reuop  6296  tfinds2  7861  soseq  8156  findcard2  9150  ac6sfi  9245  ac6num  10464  fpwwe  10632  nn1suc  12256  wrdind  14761  cjth  15156  fprodser  16005  prmind2  16744  joinlem  18438  meetlem  18452  mndind  18888  isghm  19287  islmod  20966  islindf  21943  fgcl  24016  cfinfil  24031  csdfil  24032  supfil  24033  fin1aufil  24070  quotval  26434  dfconngr1  30520  isconngr  30521  isconngr1  30522  wrdt2ind  33254  bnj62  35090  bnj610  35117  bnj976  35147  bnj106  35237  bnj125  35241  bnj154  35247  bnj155  35248  bnj526  35257  bnj540  35261  bnj591  35280  bnj609  35286  bnj893  35297  bnj1417  35410  poimirlem27  38279  sdclem2  38374  fdc  38377  fdc1  38378  lshpkrlem3  39867  hdmap1fval  42551  hdmapfval  42582  sn-isghm  43388  rabren3dioph  43525  2nn0ind  43655  zindbi  43656  onfrALTlem5  45234  onfrALTlem5VD  45576  reupr  48254