Theorem sbcie 3819

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  Vcvv 3475  [wsbc 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3777

This theorem is referenced by:  sbc2ie  3859  csbie  3928  rexopabb  5527  reuop  6289  tfinds2  7848  soseq  8140  findcard2  9160  findcard2OLD  9280  ac6sfi  9283  ac6num  10470  fpwwe  10637  nn1suc  12230  wrdind  14668  cjth  15046  fprodser  15889  prmind2  16618  joinlem  18332  meetlem  18346  mndind  18705  isghm  19086  islmod  20463  islindf  21351  fgcl  23364  cfinfil  23379  csdfil  23380  supfil  23381  fin1aufil  23418  quotval  25787  dfconngr1  29421  isconngr  29422  isconngr1  29423  wrdt2ind  32095  bnj62  33669  bnj610  33696  bnj976  33726  bnj106  33817  bnj125  33821  bnj154  33827  bnj155  33828  bnj526  33837  bnj540  33841  bnj591  33860  bnj609  33866  bnj893  33877  bnj1417  33990  poimirlem27  36453  sdclem2  36548  fdc  36551  fdc1  36552  lshpkrlem3  37920  hdmap1fval  40605  hdmapfval  40636  rabren3dioph  41486  2nn0ind  41617  zindbi  41618  onfrALTlem5  43236  onfrALTlem5VD  43579  reupr  46125