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

Theorem nfsbc 3310
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 1600 . . 3  |-  F/ y T.
2 nfsbc.1 . . . 4  |-  F/_ x A
32a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
4 nfsbc.2 . . . 4  |-  F/ x ph
54a1i 11 . . 3  |-  ( T. 
->  F/ x ph )
61, 3, 5nfsbcd 3309 . 2  |-  ( T. 
->  F/ x [. A  /  y ]. ph )
76trud 1379 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1371   F/wnf 1590   F/_wnfc 2600   [.wsbc 3288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-sbc 3289
This theorem is referenced by:  cbvralcsf  3422  opelopabf  4716  ralrnmpt  5956  dfopab2  6733  dfoprab3s  6734  mpt2xopoveq  6841  elmptrab  19527  indexa  28770  sdclem1  28782  sbcalf  29063  sbcexf  29064  sbccomieg  29274  rexrabdioph  29275  opelopabgf  30279  elovmpt2rab  30301  elovmpt2rab1  30302  ovmpt3rabdm  30305  elovmpt3rab1  30306  bnj1445  32348  bnj1446  32349  bnj1467  32358
  Copyright terms: Public domain W3C validator