Theorem sbcie 3760

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  Vcvv 3441  [wsbc 3720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sbc 3721

This theorem is referenced by:  rexopabb  5380  reuop  6112  tfinds2  7558  findcard2  8742  ac6sfi  8746  ac6num  9890  fpwwe  10057  nn1suc  11647  wrdind  14075  cjth  14454  fprodser  15295  prmind2  16019  joinlem  17613  meetlem  17627  mndind  17984  isghm  18350  islmod  19631  islindf  20501  fgcl  22483  cfinfil  22498  csdfil  22499  supfil  22500  fin1aufil  22537  quotval  24888  dfconngr1  27973  isconngr  27974  isconngr1  27975  wrdt2ind  30653  bnj62  32100  bnj610  32128  bnj976  32159  bnj106  32250  bnj125  32254  bnj154  32260  bnj155  32261  bnj526  32270  bnj540  32274  bnj591  32293  bnj609  32299  bnj893  32310  bnj1417  32423  soseq  33209  poimirlem27  35084  sdclem2  35180  fdc  35183  fdc1  35184  lshpkrlem3  36408  hdmap1fval  39092  hdmapfval  39123  rabren3dioph  39756  2nn0ind  39886  zindbi  39887  onfrALTlem5  41248  onfrALTlem5VD  41591  reupr  44039