Theorem sbcie 3470

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990  Vcvv 3200  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-sbc 3436

This theorem is referenced by:  tfinds2  7063  findcard2  8200  ac6sfi  8204  ac6num  9301  fpwwe  9468  nn1suc  11041  wrdind  13476  cjth  13843  fprodser  14679  prmind2  15398  joinlem  17011  meetlem  17025  mrcmndind  17366  isghm  17660  islmod  18867  islindf  20151  fgcl  21682  cfinfil  21697  csdfil  21698  supfil  21699  fin1aufil  21736  quotval  24047  dfconngr1  27048  isconngr  27049  isconngr1  27050  bnj62  30786  bnj610  30817  bnj976  30848  bnj106  30938  bnj125  30942  bnj154  30948  bnj155  30949  bnj526  30958  bnj540  30962  bnj591  30981  bnj609  30987  bnj893  30998  bnj1417  31109  soseq  31751  poimirlem27  33436  sdclem2  33538  fdc  33541  fdc1  33542  lshpkrlem3  34399  hdmap1fval  37086  hdmapfval  37119  rabren3dioph  37379  2nn0ind  37510  zindbi  37511  onfrALTlem5  38757