Theorem nfsbcw 3787

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2883  [wsbc 3765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-sbc 3766

This theorem is referenced by:  opelopabgf  5515  opelopabf  5520  ralrnmptw  7084  elovmporab  7653  elovmporab1w  7654  ovmpt3rabdm  7666  elovmpt3rab1  7667  dfopab2  8051  dfoprab3s  8052  ralxpes  8135  ralxp3es  8138  frpoins3xpg  8139  frpoins3xp3g  8140  mpoxopoveq  8218  elmptrab  23765  bnj1445  35075  bnj1446  35076  bnj1467  35085  indexa  37757  sdclem1  37767  sbcalf  38138  sbcexf  38139  sbccomieg  42816  rexrabdioph  42817  or2expropbilem2  47062  or2expropbi  47063  ich2exprop  47485  ichnreuop  47486  reuopreuprim  47540