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

Theorem sbcieg 3786
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2178, ax-12 2215. (Revised by GG, 12-Oct-2024.)
Hypothesis
Ref Expression
sbcieg.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
sbcieg (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem sbcieg
StepHypRef Expression
1 df-sbc 3748 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 sbcieg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32elabg 3638 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3bitrid 286 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1563  wcel 2145  {cab 2743  [wsbc 3747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748
This theorem is referenced by:  sbcie  3788  2nreu  4401  reuprg0  4664  rabsnif  4685  ralrnmptw  7079  ralrnmpt  7081  fpwwe2lem3  10606  nn1suc  12246  opfi1uzind  14538  mndind  18877  fgcl  23996  cfinfil  24011  csdfil  24012  supfil  24013  fin1aufil  24050  ifeqeqx  32798  nn0min  33078  bnj1452  35357  cdlemk35s  41573  cdlemk39s  41575  cdlemk42  41577  2nn0ind  43534  zindbi  43535  prproropreud  48113
  Copyright terms: Public domain W3C validator