Theorem sbcie 3792

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3751

This theorem is referenced by:  sbc2ie  3826  csbie  3894  rexopabb  5483  reuop  6254  tfinds2  7820  soseq  8115  findcard2  9105  ac6sfi  9207  ac6num  10408  fpwwe  10575  nn1suc  12184  wrdind  14663  cjth  15045  fprodser  15891  prmind2  16631  joinlem  18318  meetlem  18332  mndind  18731  isghm  19123  isghmOLD  19124  islmod  20746  islindf  21697  fgcl  23741  cfinfil  23756  csdfil  23757  supfil  23758  fin1aufil  23795  quotval  26176  dfconngr1  30090  isconngr  30091  isconngr1  30092  wrdt2ind  32848  bnj62  34683  bnj610  34710  bnj976  34740  bnj106  34831  bnj125  34835  bnj154  34841  bnj155  34842  bnj526  34851  bnj540  34855  bnj591  34874  bnj609  34880  bnj893  34891  bnj1417  35004  poimirlem27  37614  sdclem2  37709  fdc  37712  fdc1  37713  lshpkrlem3  39078  hdmap1fval  41763  hdmapfval  41794  sn-isghm  42634  rabren3dioph  42776  2nn0ind  42907  zindbi  42908  onfrALTlem5  44505  onfrALTlem5VD  44847  reupr  47496