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

Theorem nfsbc 3025
Description: Bound-variable hypothesis builder for class substitution. (Contributed by NM, 7-Sep-2014.) (Revised by Mario Carneiro, 12-Oct-2016.)
Hypotheses
Ref Expression
nfsbc.1  |-  F/_ x A
nfsbc.2  |-  F/ x ph
Assertion
Ref Expression
nfsbc  |-  F/ x [. A  /  y ]. ph

Proof of Theorem nfsbc
StepHypRef Expression
1 nftru 1544 . . 3  |-  F/ y  T.
2 nfsbc.1 . . . 4  |-  F/_ x A
32a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
4 nfsbc.2 . . . 4  |-  F/ x ph
54a1i 10 . . 3  |-  (  T. 
->  F/ x ph )
61, 3, 5nfsbcd 3024 . 2  |-  (  T. 
->  F/ x [. A  /  y ]. ph )
76trud 1314 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1534   F/_wnfc 2419   [.wsbc 3004
This theorem is referenced by:  cbvralcsf  3156  opelopabf  4305  ralrnmpt  5685  dfopab2  6190  dfoprab3s  6191  elmptrab  17538  indexa  26515  sdclem1  26556  sbccomieg  26973  rexrabdioph  26978  mpt2xopoveq  28201  bnj1445  29390  bnj1446  29391  bnj1467  29400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-sbc 3005
  Copyright terms: Public domain W3C validator