Theorem sbcie 3830

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  Vcvv 3480  [wsbc 3788

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  sbc2ie  3866  csbie  3934  rexopabb  5533  reuop  6313  tfinds2  7885  soseq  8184  findcard2  9204  ac6sfi  9320  ac6num  10519  fpwwe  10686  nn1suc  12288  wrdind  14760  cjth  15142  fprodser  15985  prmind2  16722  joinlem  18428  meetlem  18442  mndind  18841  isghm  19233  isghmOLD  19234  islmod  20862  islindf  21832  fgcl  23886  cfinfil  23901  csdfil  23902  supfil  23903  fin1aufil  23940  quotval  26334  dfconngr1  30207  isconngr  30208  isconngr1  30209  wrdt2ind  32938  bnj62  34734  bnj610  34761  bnj976  34791  bnj106  34882  bnj125  34886  bnj154  34892  bnj155  34893  bnj526  34902  bnj540  34906  bnj591  34925  bnj609  34931  bnj893  34942  bnj1417  35055  poimirlem27  37654  sdclem2  37749  fdc  37752  fdc1  37753  lshpkrlem3  39113  hdmap1fval  41798  hdmapfval  41829  sn-isghm  42683  rabren3dioph  42826  2nn0ind  42957  zindbi  42958  onfrALTlem5  44562  onfrALTlem5VD  44905  reupr  47509