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

Theorem nfsbc 3683
 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 𝑥𝐴
nfsbc.2 𝑥𝜑
Assertion
Ref Expression
nfsbc 𝑥[𝐴 / 𝑦]𝜑

Proof of Theorem nfsbc
StepHypRef Expression
1 nftru 1905 . . 3 𝑦
2 nfsbc.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfsbc.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfsbcd 3682 . 2 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
76mptru 1666 1 𝑥[𝐴 / 𝑦]𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1659  Ⅎwnf 1884  Ⅎwnfc 2955  [wsbc 3661 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-sbc 3662 This theorem is referenced by:  cbvralcsf  3788  opelopabgf  5220  opelopabf  5225  ralrnmpt  6616  elovmpt2rab  7139  elovmpt2rab1  7140  ovmpt3rabdm  7151  elovmpt3rab1  7152  dfopab2  7483  dfoprab3s  7484  mpt2xopoveq  7609  elmptrab  22000  bnj1445  31657  bnj1446  31658  bnj1467  31667  indexa  34070  sdclem1  34080  sbcalf  34457  sbcexf  34458  sbccomieg  38200  rexrabdioph  38201
 Copyright terms: Public domain W3C validator