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

Theorem sbcbii 3797
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 3796 . 2 (⊤ → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
43mptru 1548 1 ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wtru 1542  [wsbc 3737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-sbc 3738
This theorem is referenced by:  eqsbc2  3806  sbc3an  3807  sbccomlem  3824  sbccom  3825  sbcrext  3827  sbcabel  3832  csbcow  3868  csbco  3869  sbcnel12g  4369  sbcne12  4370  csbcom  4375  csbnestgfw  4377  csbnestgf  4382  sbccsb  4391  sbccsb2  4392  csbab  4395  2nreu  4399  sbcssg  4479  sbcop  5444  sbcrel  5734  difopabOLD  5785  sbcfung  6522  tfinds2  7796  frpoins3xpg  8068  frpoins3xp3g  8069  mpoxopovel  8147  f1od2  31521  bnj62  33201  bnj89  33202  bnj156  33209  bnj524  33218  bnj610  33228  bnj919  33248  bnj976  33258  bnj110  33339  bnj91  33342  bnj92  33343  bnj106  33349  bnj121  33351  bnj124  33352  bnj125  33353  bnj126  33354  bnj130  33355  bnj154  33359  bnj155  33360  bnj153  33361  bnj207  33362  bnj523  33368  bnj526  33369  bnj539  33372  bnj540  33373  bnj581  33389  bnj591  33392  bnj609  33398  bnj611  33399  bnj934  33416  bnj1000  33422  bnj984  33433  bnj985v  33434  bnj985  33435  bnj1040  33453  bnj1123  33467  bnj1452  33533  bnj1463  33536  sbcalf  36540  sbcexf  36541  sbccom2lem  36550  sbccom2  36551  sbccom2f  36552  sbccom2fi  36553  csbcom2fi  36554  2sbcrex  41045  2sbcrexOLD  41047  sbcrot3  41052  sbcrot5  41053  2rexfrabdioph  41057  3rexfrabdioph  41058  4rexfrabdioph  41059  6rexfrabdioph  41060  7rexfrabdioph  41061  rmydioph  41276  expdiophlem2  41284  sbcheg  41993  sbc3or  42756  trsbc  42764  onfrALTlem5  42766  eqsbc2VD  43064  sbcoreleleqVD  43083  onfrALTlem5VD  43109  ich2exprop  45595
  Copyright terms: Public domain W3C validator