Theorem sbcie 3787

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  Vcvv 3457  [wsbc 3746

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3747

This theorem is used by:  sbc2ie  3821  csbie  3889  rexopabb  5514  reuop  6298  tfinds2  7862  soseq  8157  findcard2  9152  ac6sfi  9247  ac6num  10474  fpwwe  10642  nn1suc  12266  wrdind  14776  cjth  15173  fprodser  16021  prmind2  16760  joinlem  18454  meetlem  18468  mndind  18910  isghm  19309  islmod  21014  islindf  21991  fgcl  24064  cfinfil  24079  csdfil  24080  supfil  24081  fin1aufil  24118  quotval  26482  dfconngr1  30568  isconngr  30569  isconngr1  30570  wrdt2ind  33298  bnj62  35133  bnj610  35160  bnj976  35190  bnj106  35280  bnj125  35284  bnj154  35290  bnj155  35291  bnj526  35300  bnj540  35304  bnj591  35323  bnj609  35329  bnj893  35340  bnj1417  35453  poimirlem27  38331  sdclem2  38426  fdc  38429  fdc1  38430  lshpkrlem3  39919  hdmap1fval  42603  hdmapfval  42634  sn-isghm  43438  rabren3dioph  43575  2nn0ind  43705  zindbi  43706  onfrALTlem5  45284  onfrALTlem5VD  45626  reupr  48304