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

Theorem sbcieg 3455
 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 1845 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3454 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1992  [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 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-12 2049  ax-13 2250  ax-ext 2606 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 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-v 3193  df-sbc 3423 This theorem is referenced by:  sbcie  3457  ralsng  4194  rexsng  4195  rabsnif  4233  ralrnmpt  6325  fpwwe2lem3  9400  nn1suc  10986  mrcmndind  17282  fgcl  21587  cfinfil  21602  csdfil  21603  supfil  21604  fin1aufil  21641  ifeqeqx  29199  nn0min  29400  bnj1452  30820  cdlemk35s  35691  cdlemk39s  35693  cdlemk42  35695  2nn0ind  36976  zindbi  36977  trsbcVD  38582  onfrALTlem5VD  38590
 Copyright terms: Public domain W3C validator