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

Theorem sbcie 3457
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 3455 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑𝜓))
41, 3ax-mp 5 1 ([𝐴 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987  Vcvv 3190  [wsbc 3422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192  df-sbc 3423
This theorem is referenced by:  tfinds2  7025  findcard2  8160  ac6sfi  8164  ac6num  9261  fpwwe  9428  nn1suc  11001  wrdind  13430  cjth  13793  fprodser  14623  prmind2  15341  joinlem  16951  meetlem  16965  mrcmndind  17306  isghm  17600  islmod  18807  islindf  20091  fgcl  21622  cfinfil  21637  csdfil  21638  supfil  21639  fin1aufil  21676  quotval  23985  dfconngr1  26948  isconngr  26949  isconngr1  26950  bnj62  30547  bnj610  30578  bnj976  30609  bnj106  30699  bnj125  30703  bnj154  30709  bnj155  30710  bnj526  30719  bnj540  30723  bnj591  30742  bnj609  30748  bnj893  30759  bnj1417  30870  soseq  31505  poimirlem27  33107  sdclem2  33209  fdc  33212  fdc1  33213  lshpkrlem3  33918  hdmap1fval  36605  hdmapfval  36638  rabren3dioph  36898  2nn0ind  37029  zindbi  37030  onfrALTlem5  38278
  Copyright terms: Public domain W3C validator