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

Theorem sbcieg 3664
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 2010 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3663 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wcel 2157  [wsbc 3631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-v 3385  df-sbc 3632
This theorem is referenced by:  sbcie  3666  ralsng  4407  rexsng  4408  rabsnif  4445  ralrnmpt  6592  fpwwe2lem3  9741  nn1suc  11333  opfi1uzind  13528  mrcmndind  17678  fgcl  22007  cfinfil  22022  csdfil  22023  supfil  22024  fin1aufil  22061  ifeqeqx  29871  nn0min  30077  bnj1452  31629  cdlemk35s  36950  cdlemk39s  36952  cdlemk42  36954  2nn0ind  38283  zindbi  38284
  Copyright terms: Public domain W3C validator