Theorem sbcie 3697

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1656   ∈ wcel 2164  Vcvv 3414  [wsbc 3662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-v 3416  df-sbc 3663

This theorem is referenced by:  tfinds2  7324  findcard2  8469  ac6sfi  8473  ac6num  9616  fpwwe  9783  nn1suc  11373  wrdind  13812  wrdindOLD  13813  cjth  14220  fprodser  15052  prmind2  15770  joinlem  17364  meetlem  17378  mrcmndind  17719  isghm  18011  islmod  19223  islindf  20518  fgcl  22052  cfinfil  22067  csdfil  22068  supfil  22069  fin1aufil  22106  quotval  24446  dfconngr1  27553  isconngr  27554  isconngr1  27555  bnj62  31324  bnj610  31352  bnj976  31383  bnj106  31473  bnj125  31477  bnj154  31483  bnj155  31484  bnj526  31493  bnj540  31497  bnj591  31516  bnj609  31522  bnj893  31533  bnj1417  31644  soseq  32282  cnfinltrel  33779  poimirlem27  33973  sdclem2  34073  fdc  34076  fdc1  34077  lshpkrlem3  35180  hdmap1fval  37864  hdmapfval  37895  rabren3dioph  38216  2nn0ind  38346  zindbi  38347  onfrALTlem5  39579  onfrALTlem5VD  39932