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

Theorem nfsbc 3300
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 1687 . . 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 3299 . 2  |-  ( T. 
->  F/ x [. A  /  y ]. ph )
76trud 1463 1  |-  F/ x [. A  /  y ]. ph
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1455   F/wnf 1677   F/_wnfc 2589   [.wsbc 3278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-sbc 3279
This theorem is referenced by:  cbvralcsf  3406  opelopabgf  4734  opelopabf  4739  ralrnmpt  6053  elovmpt2rab  6541  elovmpt2rab1  6542  ovmpt3rabdm  6552  elovmpt3rab1  6553  dfopab2  6873  dfoprab3s  6874  mpt2xopoveq  6991  elmptrab  20890  bnj1445  29901  bnj1446  29902  bnj1467  29911  indexa  32104  sdclem1  32116  sbcalf  32396  sbcexf  32397  sbccomieg  35680  rexrabdioph  35681
  Copyright terms: Public domain W3C validator