Theorem sbcie 3821

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  Vcvv 3475  [wsbc 3778

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  sbc2ie  3861  csbie  3930  rexopabb  5529  reuop  6293  tfinds2  7853  soseq  8145  findcard2  9164  findcard2OLD  9284  ac6sfi  9287  ac6num  10474  fpwwe  10641  nn1suc  12234  wrdind  14672  cjth  15050  fprodser  15893  prmind2  16622  joinlem  18336  meetlem  18350  mndind  18709  isghm  19092  islmod  20475  islindf  21367  fgcl  23382  cfinfil  23397  csdfil  23398  supfil  23399  fin1aufil  23436  quotval  25805  dfconngr1  29441  isconngr  29442  isconngr1  29443  wrdt2ind  32117  bnj62  33731  bnj610  33758  bnj976  33788  bnj106  33879  bnj125  33883  bnj154  33889  bnj155  33890  bnj526  33899  bnj540  33903  bnj591  33922  bnj609  33928  bnj893  33939  bnj1417  34052  poimirlem27  36515  sdclem2  36610  fdc  36613  fdc1  36614  lshpkrlem3  37982  hdmap1fval  40667  hdmapfval  40698  rabren3dioph  41553  2nn0ind  41684  zindbi  41685  onfrALTlem5  43303  onfrALTlem5VD  43646  reupr  46190