MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcie Structured version   Visualization version   GIF version

Theorem sbcie 3810
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
StepHypRef Expression
1 sbcie.1 . 2 𝐴 ∈ V
2 sbcie.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3808 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑𝜓))
41, 3ax-mp 5 1 ([𝐴 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1530  wcel 2107  Vcvv 3493  [wsbc 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495  df-sbc 3771
This theorem is referenced by:  rexopabb  5406  reuop  6137  tfinds2  7570  findcard2  8750  ac6sfi  8754  ac6num  9893  fpwwe  10060  nn1suc  11651  wrdind  14076  cjth  14454  fprodser  15295  prmind2  16021  joinlem  17613  meetlem  17627  mndind  17984  isghm  18350  islmod  19630  islindf  20948  fgcl  22478  cfinfil  22493  csdfil  22494  supfil  22495  fin1aufil  22532  quotval  24873  dfconngr1  27959  isconngr  27960  isconngr1  27961  wrdt2ind  30620  bnj62  31978  bnj610  32006  bnj976  32037  bnj106  32128  bnj125  32132  bnj154  32138  bnj155  32139  bnj526  32148  bnj540  32152  bnj591  32171  bnj609  32177  bnj893  32188  bnj1417  32301  soseq  33084  poimirlem27  34906  sdclem2  35004  fdc  35007  fdc1  35008  lshpkrlem3  36235  hdmap1fval  38919  hdmapfval  38950  rabren3dioph  39397  2nn0ind  39527  zindbi  39528  onfrALTlem5  40861  onfrALTlem5VD  41204  reupr  43669
  Copyright terms: Public domain W3C validator