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

Step	Hyp	Ref	Expression
1		nftru 1905	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbc.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcd 3682	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1666	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

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