Theorem sbcie 3848

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  Vcvv 3488  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbc2ie  3887  csbie  3957  rexopabb  5547  reuop  6324  tfinds2  7901  soseq  8200  findcard2  9230  ac6sfi  9348  ac6num  10548  fpwwe  10715  nn1suc  12315  wrdind  14770  cjth  15152  fprodser  15997  prmind2  16732  joinlem  18453  meetlem  18467  mndind  18863  isghm  19255  isghmOLD  19256  islmod  20884  islindf  21855  fgcl  23907  cfinfil  23922  csdfil  23923  supfil  23924  fin1aufil  23961  quotval  26352  dfconngr1  30220  isconngr  30221  isconngr1  30222  wrdt2ind  32920  bnj62  34696  bnj610  34723  bnj976  34753  bnj106  34844  bnj125  34848  bnj154  34854  bnj155  34855  bnj526  34864  bnj540  34868  bnj591  34887  bnj609  34893  bnj893  34904  bnj1417  35017  poimirlem27  37607  sdclem2  37702  fdc  37705  fdc1  37706  lshpkrlem3  39068  hdmap1fval  41753  hdmapfval  41784  sn-isghm  42628  rabren3dioph  42771  2nn0ind  42902  zindbi  42903  onfrALTlem5  44513  onfrALTlem5VD  44856  reupr  47396