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

Theorem sbcieg 3814
 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 1908 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3813 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   = wceq 1530   ∈ wcel 2107  [wsbc 3776 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 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-v 3502  df-sbc 3777 This theorem is referenced by:  sbcie  3816  2nreu  4396  ralsngOLD  4607  rexsngOLD  4608  reuprg0  4637  rabsnif  4658  ralrnmptw  6856  ralrnmpt  6858  fpwwe2lem3  10044  nn1suc  11648  opfi1uzind  13849  mndind  17975  fgcl  22402  cfinfil  22417  csdfil  22418  supfil  22419  fin1aufil  22456  ifeqeqx  30211  nn0min  30450  bnj1452  32208  cdlemk35s  37940  cdlemk39s  37942  cdlemk42  37944  2nn0ind  39407  zindbi  39408  prproropreud  43503
 Copyright terms: Public domain W3C validator