Theorem sbcie 3784

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3442  [wsbc 3742

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  sbc2ie  3818  csbie  3886  rexopabb  5484  reuop  6259  tfinds2  7816  soseq  8111  findcard2  9101  ac6sfi  9196  ac6num  10401  fpwwe  10569  nn1suc  12179  wrdind  14657  cjth  15038  fprodser  15884  prmind2  16624  joinlem  18316  meetlem  18330  mndind  18765  isghm  19156  isghmOLD  19157  islmod  20827  islindf  21779  fgcl  23834  cfinfil  23849  csdfil  23850  supfil  23851  fin1aufil  23888  quotval  26268  dfconngr1  30275  isconngr  30276  isconngr1  30277  wrdt2ind  33045  bnj62  34896  bnj610  34923  bnj976  34953  bnj106  35043  bnj125  35047  bnj154  35053  bnj155  35054  bnj526  35063  bnj540  35067  bnj591  35086  bnj609  35092  bnj893  35103  bnj1417  35216  poimirlem27  37895  sdclem2  37990  fdc  37993  fdc1  37994  lshpkrlem3  39485  hdmap1fval  42169  hdmapfval  42200  sn-isghm  43028  rabren3dioph  43169  2nn0ind  43299  zindbi  43300  onfrALTlem5  44895  onfrALTlem5VD  45237  reupr  47879