Theorem sbcie 3437

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  Vcvv 3173  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403

This theorem is referenced by:  tfinds2  6955  findcard2  8085  ac6sfi  8089  ac6num  9184  fpwwe  9347  nn1suc  10918  wrdind  13328  cjth  13691  fprodser  14518  prmind2  15236  joinlem  16834  meetlem  16848  mrcmndind  17189  isghm  17483  islmod  18690  islindf  19970  fgcl  21492  cfinfil  21507  csdfil  21508  supfil  21509  fin1aufil  21546  quotval  23851  bnj62  30040  bnj610  30071  bnj976  30102  bnj106  30192  bnj125  30196  bnj154  30202  bnj155  30203  bnj526  30212  bnj540  30216  bnj591  30235  bnj609  30241  bnj893  30252  bnj1417  30363  soseq  30995  poimirlem27  32606  sdclem2  32708  fdc  32711  fdc1  32712  lshpkrlem3  33417  hdmap1fval  36104  hdmapfval  36137  rabren3dioph  36397  2nn0ind  36528  zindbi  36529  onfrALTlem5  37778  dfconngr1  41355  isconngr  41356  isconngr1  41357