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

Theorem sbcbii 3826
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 3824 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43mptru 1535 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wtru 1529  [wsbc 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-sbc 3770
This theorem is referenced by:  eqsbc3r  3834  sbc3an  3835  sbccomlem  3850  sbccom  3851  sbcrext  3853  sbcabel  3858  csbcow  3895  csbco  3896  sbcnel12g  4360  sbcne12  4361  csbcom  4366  csbnestgfw  4368  csbnestgf  4373  sbccsb  4382  sbccsb2  4383  csbab  4386  2nreu  4389  sbcssg  4459  sbcop  5371  sbcrel  5648  difopab  5695  sbcfung  6372  tfinds2  7567  mpoxopovel  7875  f1od2  30383  bnj62  31889  bnj89  31890  bnj156  31897  bnj524  31907  bnj610  31917  bnj919  31937  bnj976  31948  bnj110  32029  bnj91  32032  bnj92  32033  bnj106  32039  bnj121  32041  bnj124  32042  bnj125  32043  bnj126  32044  bnj130  32045  bnj154  32049  bnj155  32050  bnj153  32051  bnj207  32052  bnj523  32058  bnj526  32059  bnj539  32062  bnj540  32063  bnj581  32079  bnj591  32082  bnj609  32088  bnj611  32089  bnj934  32106  bnj1000  32112  bnj984  32123  bnj985  32124  bnj1040  32141  bnj1123  32155  bnj1452  32221  bnj1463  32224  sbcalf  35273  sbcexf  35274  sbccom2lem  35283  sbccom2  35284  sbccom2f  35285  sbccom2fi  35286  csbcom2fi  35287  2sbcrex  39259  2sbcrexOLD  39261  sbcrot3  39266  sbcrot5  39267  2rexfrabdioph  39271  3rexfrabdioph  39272  4rexfrabdioph  39273  6rexfrabdioph  39274  7rexfrabdioph  39275  rmydioph  39489  expdiophlem2  39497  sbcheg  40003  sbc3or  40743  trsbc  40751  onfrALTlem5  40753  eqsbc3rVD  41051  sbcoreleleqVD  41070  onfrALTlem5VD  41096  ich2exprop  43510
  Copyright terms: Public domain W3C validator