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

Theorem sbcieg 3501
 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 1883 . 2 𝑥𝜓
2 sbcieg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
31, 2sbciegf 3500 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   ∈ wcel 2030  [wsbc 3468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469 This theorem is referenced by:  sbcie  3503  ralsng  4250  rexsng  4251  rabsnif  4290  ralrnmpt  6408  fpwwe2lem3  9493  nn1suc  11079  opfi1uzind  13321  mrcmndind  17413  fgcl  21729  cfinfil  21744  csdfil  21745  supfil  21746  fin1aufil  21783  ifeqeqx  29487  nn0min  29695  bnj1452  31246  cdlemk35s  36542  cdlemk39s  36544  cdlemk42  36546  2nn0ind  37827  zindbi  37828  trsbcVD  39427
 Copyright terms: Public domain W3C validator