Theorem nfsbcw 3760

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3763 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)

Hypotheses

Ref	Expression
nfsbcw.1	⊢ Ⅎ𝑥𝐴
nfsbcw.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfsbcw	⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfsbcw

Step	Hyp	Ref	Expression
1		nftru 1805	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3759	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1548	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2881  [wsbc 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-sbc 3739

This theorem is referenced by:  opelopabgf  5485  opelopabf  5490  ralrnmptw  7036  elovmporab  7601  elovmporab1w  7602  ovmpt3rabdm  7614  elovmpt3rab1  7615  dfopab2  7993  dfoprab3s  7994  ralxpes  8075  ralxp3es  8078  frpoins3xpg  8079  frpoins3xp3g  8080  mpoxopoveq  8158  elmptrab  23752  bnj1445  35067  bnj1446  35068  bnj1467  35077  indexa  37783  sdclem1  37793  sbcalf  38164  sbcexf  38165  sbccomieg  42900  rexrabdioph  42901  or2expropbilem2  47147  or2expropbi  47148  ich2exprop  47585  ichnreuop  47586  reuopreuprim  47640