Theorem nfsbcw 3761

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3764 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2371. (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 3760	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1548	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2877  [wsbc 3739

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-sbc 3740

This theorem is referenced by:  opelopabgf  5478  opelopabf  5483  ralrnmptw  7022  elovmporab  7587  elovmporab1w  7588  ovmpt3rabdm  7600  elovmpt3rab1  7601  dfopab2  7979  dfoprab3s  7980  ralxpes  8061  ralxp3es  8064  frpoins3xpg  8065  frpoins3xp3g  8066  mpoxopoveq  8144  elmptrab  23735  bnj1445  35046  bnj1446  35047  bnj1467  35056  indexa  37752  sdclem1  37762  sbcalf  38133  sbcexf  38134  sbccomieg  42805  rexrabdioph  42806  or2expropbilem2  47043  or2expropbi  47044  ich2exprop  47481  ichnreuop  47482  reuopreuprim  47536