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

Theorem sbcbii 3827
Description: Formula-building inference for class substitution. (Contributed by NM, 11-Nov-2005.)
Hypothesis
Ref Expression
sbcbii.1 (𝜑𝜓)
Assertion
Ref Expression
sbcbii ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)

Proof of Theorem sbcbii
StepHypRef Expression
1 sbcbii.1 . . . 4 (𝜑𝜓)
21a1i 11 . . 3 (⊤ → (𝜑𝜓))
32sbcbidv 3825 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43mptru 1537 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wtru 1531  [wsbc 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1533  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-sbc 3771
This theorem is referenced by:  eqsbc3r  3835  sbc3an  3836  sbccomlem  3851  sbccom  3852  sbcrext  3854  sbcabel  3859  csbcow  3896  csbco  3897  sbcnel12g  4361  sbcne12  4362  csbcom  4367  csbnestgfw  4369  csbnestgf  4374  sbccsb  4383  sbccsb2  4384  csbab  4387  2nreu  4391  sbcssg  4461  sbcop  5371  sbcrel  5648  difopab  5695  sbcfung  6372  tfinds2  7570  mpoxopovel  7878  f1od2  30449  bnj62  31978  bnj89  31979  bnj156  31986  bnj524  31996  bnj610  32006  bnj919  32026  bnj976  32037  bnj110  32118  bnj91  32121  bnj92  32122  bnj106  32128  bnj121  32130  bnj124  32131  bnj125  32132  bnj126  32133  bnj130  32134  bnj154  32138  bnj155  32139  bnj153  32140  bnj207  32141  bnj523  32147  bnj526  32148  bnj539  32151  bnj540  32152  bnj581  32168  bnj591  32171  bnj609  32177  bnj611  32178  bnj934  32195  bnj1000  32201  bnj984  32212  bnj985v  32213  bnj985  32214  bnj1040  32232  bnj1123  32246  bnj1452  32312  bnj1463  32315  sbcalf  35379  sbcexf  35380  sbccom2lem  35389  sbccom2  35390  sbccom2f  35391  sbccom2fi  35392  csbcom2fi  35393  2sbcrex  39366  2sbcrexOLD  39368  sbcrot3  39373  sbcrot5  39374  2rexfrabdioph  39378  3rexfrabdioph  39379  4rexfrabdioph  39380  6rexfrabdioph  39381  7rexfrabdioph  39382  rmydioph  39596  expdiophlem2  39604  sbcheg  40110  sbc3or  40851  trsbc  40859  onfrALTlem5  40861  eqsbc3rVD  41159  sbcoreleleqVD  41178  onfrALTlem5VD  41204  ich2exprop  43618
  Copyright terms: Public domain W3C validator