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

Theorem sbcieg 3807
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)
Hypothesis
Ref Expression
sbcieg.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
sbcieg (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem sbcieg
StepHypRef Expression
1 nfv 1906 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3806 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  [wsbc 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-v 3494  df-sbc 3770
This theorem is referenced by:  sbcie  3809  2nreu  4389  ralsngOLD  4600  rexsngOLD  4601  reuprg0  4630  rabsnif  4651  ralrnmptw  6852  ralrnmpt  6854  fpwwe2lem3  10043  nn1suc  11647  opfi1uzind  13847  mndind  17980  fgcl  22414  cfinfil  22429  csdfil  22430  supfil  22431  fin1aufil  22468  ifeqeqx  30224  nn0min  30463  bnj1452  32221  cdlemk35s  37953  cdlemk39s  37955  cdlemk42  37957  2nn0ind  39420  zindbi  39421  prproropreud  43548
  Copyright terms: Public domain W3C validator