Theorem sbcie 3794

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  Vcvv 3463  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754

This theorem is referenced by:  sbc2ie  3828  csbie  3896  rexopabb  5510  reuop  6291  tfinds2  7856  soseq  8151  findcard2  9145  ac6sfi  9240  ac6num  10459  fpwwe  10627  nn1suc  12251  wrdind  14755  cjth  15150  fprodser  15999  prmind2  16739  joinlem  18433  meetlem  18447  mndind  18883  isghm  19282  islmod  20959  islindf  21927  fgcl  24000  cfinfil  24015  csdfil  24016  supfil  24017  fin1aufil  24054  quotval  26418  dfconngr1  30476  isconngr  30477  isconngr1  30478  wrdt2ind  33210  bnj62  35050  bnj610  35077  bnj976  35107  bnj106  35197  bnj125  35201  bnj154  35207  bnj155  35208  bnj526  35217  bnj540  35221  bnj591  35240  bnj609  35246  bnj893  35257  bnj1417  35370  poimirlem27  38181  sdclem2  38276  fdc  38279  fdc1  38280  lshpkrlem3  39771  hdmap1fval  42455  hdmapfval  42486  sn-isghm  43290  rabren3dioph  43427  2nn0ind  43557  zindbi  43558  onfrALTlem5  45136  onfrALTlem5VD  45478  reupr  48153