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

Theorem nfsbc 3346
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 1631 . . 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 3345 . 2  |-  ( T. 
->  F/ x [. A  /  y ]. ph )
76trud 1407 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1399   F/wnf 1621   F/_wnfc 2602   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-sbc 3325
This theorem is referenced by:  cbvralcsf  3452  opelopabgf  4756  opelopabf  4761  ralrnmpt  6016  elovmpt2rab  6494  elovmpt2rab1  6495  ovmpt3rabdm  6508  elovmpt3rab1  6509  dfopab2  6827  dfoprab3s  6828  mpt2xopoveq  6939  elmptrab  20497  indexa  30467  sdclem1  30479  sbcalf  30760  sbcexf  30761  sbccomieg  30969  rexrabdioph  30970  bnj1445  34520  bnj1446  34521  bnj1467  34530
  Copyright terms: Public domain W3C validator