Theorem sbcie 3807

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108  Vcvv 3459  [wsbc 3765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  sbc2ie  3841  csbie  3909  rexopabb  5503  reuop  6282  tfinds2  7859  soseq  8158  findcard2  9178  ac6sfi  9292  ac6num  10493  fpwwe  10660  nn1suc  12262  wrdind  14740  cjth  15122  fprodser  15965  prmind2  16704  joinlem  18393  meetlem  18407  mndind  18806  isghm  19198  isghmOLD  19199  islmod  20821  islindf  21772  fgcl  23816  cfinfil  23831  csdfil  23832  supfil  23833  fin1aufil  23870  quotval  26252  dfconngr1  30169  isconngr  30170  isconngr1  30171  wrdt2ind  32929  bnj62  34751  bnj610  34778  bnj976  34808  bnj106  34899  bnj125  34903  bnj154  34909  bnj155  34910  bnj526  34919  bnj540  34923  bnj591  34942  bnj609  34948  bnj893  34959  bnj1417  35072  poimirlem27  37671  sdclem2  37766  fdc  37769  fdc1  37770  lshpkrlem3  39130  hdmap1fval  41815  hdmapfval  41846  sn-isghm  42696  rabren3dioph  42838  2nn0ind  42969  zindbi  42970  onfrALTlem5  44567  onfrALTlem5VD  44909  reupr  47536