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

Theorem nfsbc 3182
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 1563 . . 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 3181 . 2  |-  (  T. 
->  F/ x [. A  /  y ]. ph )
76trud 1332 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/wnf 1553   F/_wnfc 2559   [.wsbc 3161
This theorem is referenced by:  cbvralcsf  3311  opelopabf  4479  ralrnmpt  5878  dfopab2  6401  dfoprab3s  6402  mpt2xopoveq  6470  elmptrab  17859  indexa  26435  sdclem1  26447  sbccomieg  26849  rexrabdioph  26854  opelopabgf  28071  bnj1445  29413  bnj1446  29414  bnj1467  29423
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-sbc 3162
  Copyright terms: Public domain W3C validator