Theorem sbcie 3798

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3450  [wsbc 3756

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757

This theorem is referenced by:  sbc2ie  3832  csbie  3900  rexopabb  5491  reuop  6269  tfinds2  7843  soseq  8141  findcard2  9134  ac6sfi  9238  ac6num  10439  fpwwe  10606  nn1suc  12215  wrdind  14694  cjth  15076  fprodser  15922  prmind2  16662  joinlem  18349  meetlem  18363  mndind  18762  isghm  19154  isghmOLD  19155  islmod  20777  islindf  21728  fgcl  23772  cfinfil  23787  csdfil  23788  supfil  23789  fin1aufil  23826  quotval  26207  dfconngr1  30124  isconngr  30125  isconngr1  30126  wrdt2ind  32882  bnj62  34717  bnj610  34744  bnj976  34774  bnj106  34865  bnj125  34869  bnj154  34875  bnj155  34876  bnj526  34885  bnj540  34889  bnj591  34908  bnj609  34914  bnj893  34925  bnj1417  35038  poimirlem27  37648  sdclem2  37743  fdc  37746  fdc1  37747  lshpkrlem3  39112  hdmap1fval  41797  hdmapfval  41828  sn-isghm  42668  rabren3dioph  42810  2nn0ind  42941  zindbi  42942  onfrALTlem5  44539  onfrALTlem5VD  44881  reupr  47527