Theorem sbcie 3766

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  Vcvv 3433  [wsbc 3725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-sbc 3726

This theorem is referenced by:  sbc2ie  3800  csbie  3868  rexopabb  5473  reuop  6248  tfinds2  7808  soseq  8103  findcard2  9093  ac6sfi  9188  ac6num  10396  fpwwe  10564  nn1suc  12191  wrdind  14679  cjth  15060  fprodser  15909  prmind2  16649  joinlem  18342  meetlem  18356  mndind  18791  isghm  19185  isghmOLD  19186  islmod  20858  islindf  21791  fgcl  23865  cfinfil  23880  csdfil  23881  supfil  23882  fin1aufil  23919  quotval  26280  dfconngr1  30280  isconngr  30281  isconngr1  30282  wrdt2ind  33036  bnj62  34918  bnj610  34945  bnj976  34975  bnj106  35065  bnj125  35069  bnj154  35075  bnj155  35076  bnj526  35085  bnj540  35089  bnj591  35108  bnj609  35114  bnj893  35125  bnj1417  35238  poimirlem27  38029  sdclem2  38124  fdc  38127  fdc1  38128  lshpkrlem3  39619  hdmap1fval  42303  hdmapfval  42334  sn-isghm  43138  rabren3dioph  43275  2nn0ind  43405  zindbi  43406  onfrALTlem5  45001  onfrALTlem5VD  45343  reupr  48011