Theorem sbcie 3759

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  Vcvv 3432  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbc2ie  3799  csbie  3868  rexopabb  5441  reuop  6196  tfinds2  7710  findcard2  8947  findcard2OLD  9056  ac6sfi  9058  ac6num  10235  fpwwe  10402  nn1suc  11995  wrdind  14435  cjth  14814  fprodser  15659  prmind2  16390  joinlem  18101  meetlem  18115  mndind  18466  isghm  18834  islmod  20127  islindf  21019  fgcl  23029  cfinfil  23044  csdfil  23045  supfil  23046  fin1aufil  23083  quotval  25452  dfconngr1  28552  isconngr  28553  isconngr1  28554  wrdt2ind  31225  bnj62  32699  bnj610  32727  bnj976  32757  bnj106  32848  bnj125  32852  bnj154  32858  bnj155  32859  bnj526  32868  bnj540  32872  bnj591  32891  bnj609  32897  bnj893  32908  bnj1417  33021  soseq  33803  poimirlem27  35804  sdclem2  35900  fdc  35903  fdc1  35904  lshpkrlem3  37126  hdmap1fval  39810  hdmapfval  39841  rabren3dioph  40637  2nn0ind  40767  zindbi  40768  onfrALTlem5  42162  onfrALTlem5VD  42505  reupr  44974