Theorem nfsbcw 3796

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3799 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2365. (Revised by Gino Giotto, 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 1798	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3795	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1540	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1534  Ⅎwnf 1777  Ⅎwnfc 2875  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-sbc 3775

This theorem is referenced by:  opelopabgf  5541  opelopabf  5546  ralrnmptw  7101  elovmporab  7665  elovmporab1w  7666  ovmpt3rabdm  7678  elovmpt3rab1  7679  dfopab2  8055  dfoprab3s  8056  ralxpes  8139  ralxp3es  8142  frpoins3xpg  8143  frpoins3xp3g  8144  mpoxopoveq  8223  elmptrab  23761  bnj1445  34745  bnj1446  34746  bnj1467  34755  indexa  37276  sdclem1  37286  sbcalf  37657  sbcexf  37658  sbccomieg  42278  rexrabdioph  42279  or2expropbilem2  46478  or2expropbi  46479  ich2exprop  46874  ichnreuop  46875  reuopreuprim  46929