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

Theorem sbcieg 3620
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 1995 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3619 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145  [wsbc 3587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588
This theorem is referenced by:  sbcie  3622  ralsng  4356  rexsng  4357  rabsnif  4394  ralrnmpt  6511  fpwwe2lem3  9657  nn1suc  11243  opfi1uzind  13485  mrcmndind  17574  fgcl  21902  cfinfil  21917  csdfil  21918  supfil  21919  fin1aufil  21956  ifeqeqx  29699  nn0min  29907  bnj1452  31458  cdlemk35s  36746  cdlemk39s  36748  cdlemk42  36750  2nn0ind  38036  zindbi  38037  trsbcVD  39635
  Copyright terms: Public domain W3C validator