Theorem nfsbcw 3769

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

Syntax hints:  ⊤wtru 1564  Ⅎwnf 1806  Ⅎwnfc 2912  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-sbc 3748

This theorem is referenced by:  opelopabgf  5516  opelopabf  5521  ralrnmptw  7079  elovmporab  7646  elovmporab1w  7647  ovmpt3rabdm  7659  elovmpt3rab1  7660  dfopab2  8037  dfoprab3s  8038  ralxpes  8120  ralxp3es  8123  frpoins3xpg  8124  frpoins3xp3g  8125  mpoxopoveq  8203  elmptrab  23945  bnj1445  35349  bnj1446  35350  bnj1467  35359  indexa  38244  sdclem1  38254  sbcalf  38625  sbcexf  38626  sbccomieg  43382  rexrabdioph  43383  or2expropbilem2  47625  or2expropbi  47626  ich2exprop  48075  ichnreuop  48076  reuopreuprim  48130