Theorem nfsbcw 3800

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786  Ⅎwnfc 2884  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-sbc 3779

This theorem is referenced by:  opelopabgf  5541  opelopabf  5546  ralrnmptw  7096  elovmporab  7652  elovmporab1w  7653  ovmpt3rabdm  7665  elovmpt3rab1  7666  dfopab2  8038  dfoprab3s  8039  ralxpes  8122  ralxp3es  8125  frpoins3xpg  8126  frpoins3xp3g  8127  mpoxopoveq  8204  elmptrab  23331  bnj1445  34055  bnj1446  34056  bnj1467  34065  indexa  36601  sdclem1  36611  sbcalf  36982  sbcexf  36983  sbccomieg  41531  rexrabdioph  41532  or2expropbilem2  45743  or2expropbi  45744  ich2exprop  46139  ichnreuop  46140  reuopreuprim  46194