Theorem sbcie 3834

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  Vcvv 3477  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791

This theorem is referenced by:  sbc2ie  3873  csbie  3943  rexopabb  5537  reuop  6314  tfinds2  7884  soseq  8182  findcard2  9202  ac6sfi  9317  ac6num  10516  fpwwe  10683  nn1suc  12285  wrdind  14756  cjth  15138  fprodser  15981  prmind2  16718  joinlem  18440  meetlem  18454  mndind  18853  isghm  19245  isghmOLD  19246  islmod  20878  islindf  21849  fgcl  23901  cfinfil  23916  csdfil  23917  supfil  23918  fin1aufil  23955  quotval  26348  dfconngr1  30216  isconngr  30217  isconngr1  30218  wrdt2ind  32922  bnj62  34712  bnj610  34739  bnj976  34769  bnj106  34860  bnj125  34864  bnj154  34870  bnj155  34871  bnj526  34880  bnj540  34884  bnj591  34903  bnj609  34909  bnj893  34920  bnj1417  35033  poimirlem27  37633  sdclem2  37728  fdc  37731  fdc1  37732  lshpkrlem3  39093  hdmap1fval  41778  hdmapfval  41809  sn-isghm  42659  rabren3dioph  42802  2nn0ind  42933  zindbi  42934  onfrALTlem5  44539  onfrALTlem5VD  44882  reupr  47446