Theorem nfsbc 3457

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 1730	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbc.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcd 3456	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	trud 1493	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1484  Ⅎwnf 1708  Ⅎwnfc 2751  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-sbc 3436

This theorem is referenced by:  cbvralcsf  3565  opelopabgf  4995  opelopabf  5000  ralrnmpt  6368  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rabdm  6892  elovmpt3rab1  6893  dfopab2  7222  dfoprab3s  7223  mpt2xopoveq  7345  elmptrab  21630  bnj1445  31112  bnj1446  31113  bnj1467  31122  indexa  33528  sdclem1  33539  sbcalf  33917  sbcexf  33918  sbccomieg  37357  rexrabdioph  37358