Theorem sbcie 3795

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3447  [wsbc 3753

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 3754

This theorem is referenced by:  sbc2ie  3829  csbie  3897  rexopabb  5488  reuop  6266  tfinds2  7840  soseq  8138  findcard2  9128  ac6sfi  9231  ac6num  10432  fpwwe  10599  nn1suc  12208  wrdind  14687  cjth  15069  fprodser  15915  prmind2  16655  joinlem  18342  meetlem  18356  mndind  18755  isghm  19147  isghmOLD  19148  islmod  20770  islindf  21721  fgcl  23765  cfinfil  23780  csdfil  23781  supfil  23782  fin1aufil  23819  quotval  26200  dfconngr1  30117  isconngr  30118  isconngr1  30119  wrdt2ind  32875  bnj62  34710  bnj610  34737  bnj976  34767  bnj106  34858  bnj125  34862  bnj154  34868  bnj155  34869  bnj526  34878  bnj540  34882  bnj591  34901  bnj609  34907  bnj893  34918  bnj1417  35031  poimirlem27  37641  sdclem2  37736  fdc  37739  fdc1  37740  lshpkrlem3  39105  hdmap1fval  41790  hdmapfval  41821  sn-isghm  42661  rabren3dioph  42803  2nn0ind  42934  zindbi  42935  onfrALTlem5  44532  onfrALTlem5VD  44874  reupr  47523