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

Theorem sbcieg 3827
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2140, ax-12 2176. (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 3788 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 sbcieg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32elabg 3675 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3bitrid 283 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  wcel 2107  {cab 2713  [wsbc 3787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-sbc 3788
This theorem is referenced by:  sbcie  3829  2nreu  4443  reuprg0  4701  rabsnif  4722  ralrnmptw  7113  ralrnmpt  7115  fpwwe2lem3  10674  nn1suc  12289  opfi1uzind  14551  mndind  18842  fgcl  23887  cfinfil  23902  csdfil  23903  supfil  23904  fin1aufil  23941  ifeqeqx  32556  nn0min  32823  bnj1452  35067  cdlemk35s  40940  cdlemk39s  40942  cdlemk42  40944  2nn0ind  42962  zindbi  42963  prproropreud  47501
  Copyright terms: Public domain W3C validator