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

Theorem nfsbc 3444
 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 1727 . . 3 𝑦
2 nfsbc.1 . . . 4 𝑥𝐴
32a1i 11 . . 3 (⊤ → 𝑥𝐴)
4 nfsbc.2 . . . 4 𝑥𝜑
54a1i 11 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfsbcd 3443 . 2 (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
76trud 1490 1 𝑥[𝐴 / 𝑦]𝜑
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1481  Ⅎwnf 1705  Ⅎwnfc 2748  [wsbc 3422 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-sbc 3423 This theorem is referenced by:  cbvralcsf  3551  opelopabgf  4965  opelopabf  4970  ralrnmpt  6334  elovmpt2rab  6845  elovmpt2rab1  6846  ovmpt3rabdm  6857  elovmpt3rab1  6858  dfopab2  7182  dfoprab3s  7183  mpt2xopoveq  7305  elmptrab  21570  bnj1445  30873  bnj1446  30874  bnj1467  30883  indexa  33199  sdclem1  33210  sbcalf  33588  sbcexf  33589  sbccomieg  36876  rexrabdioph  36877
 Copyright terms: Public domain W3C validator