Theorem sbcie 3779

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3437  [wsbc 3737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738

This theorem is referenced by:  sbc2ie  3813  csbie  3881  rexopabb  5473  reuop  6247  tfinds2  7802  soseq  8097  findcard2  9083  ac6sfi  9177  ac6num  10379  fpwwe  10546  nn1suc  12156  wrdind  14633  cjth  15014  fprodser  15860  prmind2  16600  joinlem  18291  meetlem  18305  mndind  18740  isghm  19131  isghmOLD  19132  islmod  20801  islindf  21753  fgcl  23796  cfinfil  23811  csdfil  23812  supfil  23813  fin1aufil  23850  quotval  26230  dfconngr1  30172  isconngr  30173  isconngr1  30174  wrdt2ind  32943  bnj62  34755  bnj610  34782  bnj976  34812  bnj106  34903  bnj125  34907  bnj154  34913  bnj155  34914  bnj526  34923  bnj540  34927  bnj591  34946  bnj609  34952  bnj893  34963  bnj1417  35076  poimirlem27  37710  sdclem2  37805  fdc  37808  fdc1  37809  lshpkrlem3  39234  hdmap1fval  41918  hdmapfval  41949  sn-isghm  42794  rabren3dioph  42935  2nn0ind  43065  zindbi  43066  onfrALTlem5  44662  onfrALTlem5VD  45004  reupr  47649