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 2397. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2397. (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 1818	. . 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 1561	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1555  Ⅎwnf 1797  Ⅎwnfc 2903  [wsbc 3739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1557  df-ex 1794  df-nf 1798  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-sbc 3740

This theorem is referenced by:  opelopabgf  5504  opelopabf  5509  ralrnmptw  7064  elovmporab  7631  elovmporab1w  7632  ovmpt3rabdm  7644  elovmpt3rab1  7645  dfopab2  8022  dfoprab3s  8023  ralxpes  8104  ralxp3es  8107  frpoins3xpg  8108  frpoins3xp3g  8109  mpoxopoveq  8187  elmptrab  23860  bnj1445  35296  bnj1446  35297  bnj1467  35306  indexa  38180  sdclem1  38190  sbcalf  38561  sbcexf  38562  sbccomieg  43318  rexrabdioph  43319  or2expropbilem2  47575  or2expropbi  47576  ich2exprop  48025  ichnreuop  48026  reuopreuprim  48080