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

Theorem nfsbc 3353
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 1609 . . 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 3352 . 2  |-  ( T. 
->  F/ x [. A  /  y ]. ph )
76trud 1388 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1380   F/wnf 1599   F/_wnfc 2615   [.wsbc 3331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-sbc 3332
This theorem is referenced by:  cbvralcsf  3467  opelopabgf  4767  opelopabf  4772  ralrnmpt  6028  elovmpt2rab  6503  elovmpt2rab1  6504  ovmpt3rabdm  6517  elovmpt3rab1  6518  dfopab2  6835  dfoprab3s  6836  mpt2xopoveq  6944  elmptrab  20063  indexa  29827  sdclem1  29839  sbcalf  30120  sbcexf  30121  sbccomieg  30330  rexrabdioph  30331  bnj1445  33179  bnj1446  33180  bnj1467  33189
  Copyright terms: Public domain W3C validator