Theorem sbcie 3814

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3496  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498  df-sbc 3775

This theorem is referenced by:  rexopabb  5417  reuop  6146  tfinds2  7580  findcard2  8760  ac6sfi  8764  ac6num  9903  fpwwe  10070  nn1suc  11662  wrdind  14086  cjth  14464  fprodser  15305  prmind2  16031  joinlem  17623  meetlem  17637  mndind  17994  isghm  18360  islmod  19640  islindf  20958  fgcl  22488  cfinfil  22503  csdfil  22504  supfil  22505  fin1aufil  22542  quotval  24883  dfconngr1  27969  isconngr  27970  isconngr1  27971  wrdt2ind  30629  bnj62  31992  bnj610  32020  bnj976  32051  bnj106  32142  bnj125  32146  bnj154  32152  bnj155  32153  bnj526  32162  bnj540  32166  bnj591  32185  bnj609  32191  bnj893  32202  bnj1417  32315  soseq  33098  poimirlem27  34921  sdclem2  35019  fdc  35022  fdc1  35023  lshpkrlem3  36250  hdmap1fval  38934  hdmapfval  38965  rabren3dioph  39419  2nn0ind  39549  zindbi  39550  onfrALTlem5  40883  onfrALTlem5VD  41226  reupr  43691