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

Theorem sbcbii 3387
Description: Formula-building inference rule 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 3386 . 2
43trud 1404 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184   wtru 1396  [.wsbc 3327
This theorem is referenced by:  sbcbiiOLD  3388  eqsbc3r  3389  sbc3an  3390  sbccomlem  3406  sbccom  3407  sbcrextOLD  3409  sbcrext  3410  sbcabel  3416  csbco  3444  sbcnel12g  3826  sbcne12  3827  sbcne12gOLD  3828  csbcom  3837  csbnestgf  3840  sbccsb  3849  sbccsbgOLD  3850  sbccsb2  3851  sbccsb2gOLD  3852  csbab  3855  csbabgOLD  3856  sbcssg  3940  sbcrel  5094  difopab  5139  sbcfung  5616  tfinds2  6698  mpt2xopovel  6967  f1od2  27547  sbcalf  30517  sbcexf  30518  sbccom2lem  30529  sbccom2  30530  sbccom2f  30531  sbccom2fi  30532  csbcom2fi  30534  2sbcrex  30718  2sbcrexOLD  30719  sbcrot3  30724  sbcrot5  30725  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  rmydioph  30956  expdiophlem2  30964  sbc3or  33302  trsbc  33311  onfrALTlem5  33314  bnj62  33773  bnj89  33774  bnj156  33783  bnj524  33793  bnj538OLD  33797  bnj610  33804  bnj919  33825  bnj976  33836  bnj110  33916  bnj91  33919  bnj92  33920  bnj106  33926  bnj121  33928  bnj124  33929  bnj125  33930  bnj126  33931  bnj130  33932  bnj154  33936  bnj155  33937  bnj153  33938  bnj207  33939  bnj523  33945  bnj526  33946  bnj539  33949  bnj540  33950  bnj581  33966  bnj591  33969  bnj609  33975  bnj611  33976  bnj934  33993  bnj1000  33999  bnj984  34010  bnj985  34011  bnj1040  34028  bnj1123  34042  bnj1452  34108  bnj1463  34111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328
  Copyright terms: Public domain W3C validator