Theorem sbcie 3779

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  Vcvv 3450  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbc2ie  3813  csbie  3881  rexopabb  5501  reuop  6296  tfinds2  7876  soseq  8179  findcard2  9184  ac6sfi  9279  ac6num  10561  fpwwe  10735  nn1suc  12361  wrdind  14876  cjth  15276  fprodser  16122  prmind2  16866  joinlem  18561  meetlem  18575  mndind  19030  isghm  19436  islmod  21145  islindf  22124  fgcl  24203  cfinfil  24218  csdfil  24219  supfil  24220  fin1aufil  24257  quotval  26619  dfconngr1  30795  isconngr  30796  isconngr1  30797  wrdt2ind  33563  bnj62  35398  bnj610  35425  bnj976  35455  bnj106  35545  bnj125  35549  bnj154  35555  bnj155  35556  bnj526  35565  bnj540  35569  bnj591  35588  bnj609  35594  bnj893  35605  bnj1417  35718  poimirlem27  38659  sdclem2  38770  fdc  38773  fdc1  38774  lshpkrlem3  40263  hdmap1fval  42947  hdmapfval  42978  sn-isghm  43778  rabren3dioph  43916  2nn0ind  44046  zindbi  44047  onfrALTlem5  45619  onfrALTlem5VD  45961  reupr  48698