Theorem sbcie 3782

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3440  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  sbc2ie  3816  csbie  3884  rexopabb  5476  reuop  6251  tfinds2  7806  soseq  8101  findcard2  9089  ac6sfi  9184  ac6num  10389  fpwwe  10557  nn1suc  12167  wrdind  14645  cjth  15026  fprodser  15872  prmind2  16612  joinlem  18304  meetlem  18318  mndind  18753  isghm  19144  isghmOLD  19145  islmod  20815  islindf  21767  fgcl  23822  cfinfil  23837  csdfil  23838  supfil  23839  fin1aufil  23876  quotval  26256  dfconngr1  30263  isconngr  30264  isconngr1  30265  wrdt2ind  33035  bnj62  34876  bnj610  34903  bnj976  34933  bnj106  35024  bnj125  35028  bnj154  35034  bnj155  35035  bnj526  35044  bnj540  35048  bnj591  35067  bnj609  35073  bnj893  35084  bnj1417  35197  poimirlem27  37848  sdclem2  37943  fdc  37946  fdc1  37947  lshpkrlem3  39372  hdmap1fval  42056  hdmapfval  42087  sn-isghm  42916  rabren3dioph  43057  2nn0ind  43187  zindbi  43188  onfrALTlem5  44783  onfrALTlem5VD  45125  reupr  47768