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

Theorem sbcieg 3832
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) Avoid ax-10 2139, ax-12 2175. (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 3792 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 sbcieg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32elabg 3677 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3bitrid 283 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wcel 2106  {cab 2712  [wsbc 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792
This theorem is referenced by:  sbcie  3835  2nreu  4450  reuprg0  4707  rabsnif  4728  ralrnmptw  7114  ralrnmpt  7116  fpwwe2lem3  10671  nn1suc  12286  opfi1uzind  14547  mndind  18854  fgcl  23902  cfinfil  23917  csdfil  23918  supfil  23919  fin1aufil  23956  ifeqeqx  32563  nn0min  32827  bnj1452  35045  cdlemk35s  40920  cdlemk39s  40922  cdlemk42  40924  2nn0ind  42934  zindbi  42935  prproropreud  47434
  Copyright terms: Public domain W3C validator