Theorem sbcie 3607

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1628   ∈ wcel 2135  Vcvv 3336  [wsbc 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-12 2192  ax-13 2387  ax-ext 2736

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-v 3338  df-sbc 3573

This theorem is referenced by:  tfinds2  7224  findcard2  8361  ac6sfi  8365  ac6num  9489  fpwwe  9656  nn1suc  11229  wrdind  13672  cjth  14038  fprodser  14874  prmind2  15596  joinlem  17208  meetlem  17222  mrcmndind  17563  isghm  17857  islmod  19065  islindf  20349  fgcl  21879  cfinfil  21894  csdfil  21895  supfil  21896  fin1aufil  21933  quotval  24242  dfconngr1  27336  isconngr  27337  isconngr1  27338  bnj62  31091  bnj610  31120  bnj976  31151  bnj106  31241  bnj125  31245  bnj154  31251  bnj155  31252  bnj526  31261  bnj540  31265  bnj591  31284  bnj609  31290  bnj893  31301  bnj1417  31412  soseq  32056  cnfinltrel  33548  poimirlem27  33745  sdclem2  33847  fdc  33850  fdc1  33851  lshpkrlem3  34898  hdmap1fval  37584  hdmapfval  37617  rabren3dioph  37877  2nn0ind  38008  zindbi  38009  onfrALTlem5  39255  onfrALTlem5VD  39616