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 206   = wceq 1540   ∈ wcel 2109  Vcvv 3438  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  sbc2ie  3820  csbie  3888  rexopabb  5475  reuop  6245  tfinds2  7804  soseq  8099  findcard2  9088  ac6sfi  9189  ac6num  10392  fpwwe  10559  nn1suc  12168  wrdind  14646  cjth  15028  fprodser  15874  prmind2  16614  joinlem  18305  meetlem  18319  mndind  18720  isghm  19112  isghmOLD  19113  islmod  20785  islindf  21737  fgcl  23781  cfinfil  23796  csdfil  23797  supfil  23798  fin1aufil  23835  quotval  26216  dfconngr1  30150  isconngr  30151  isconngr1  30152  wrdt2ind  32908  bnj62  34689  bnj610  34716  bnj976  34746  bnj106  34837  bnj125  34841  bnj154  34847  bnj155  34848  bnj526  34857  bnj540  34861  bnj591  34880  bnj609  34886  bnj893  34897  bnj1417  35010  poimirlem27  37629  sdclem2  37724  fdc  37727  fdc1  37728  lshpkrlem3  39093  hdmap1fval  41778  hdmapfval  41809  sn-isghm  42649  rabren3dioph  42791  2nn0ind  42921  zindbi  42922  onfrALTlem5  44519  onfrALTlem5VD  44861  reupr  47510