Theorem nfsbcw 3766

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876  [wsbc 3744

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-sbc 3745

This theorem is referenced by:  opelopabgf  5487  opelopabf  5492  ralrnmptw  7032  elovmporab  7599  elovmporab1w  7600  ovmpt3rabdm  7612  elovmpt3rab1  7613  dfopab2  7994  dfoprab3s  7995  ralxpes  8076  ralxp3es  8079  frpoins3xpg  8080  frpoins3xp3g  8081  mpoxopoveq  8159  elmptrab  23730  bnj1445  35010  bnj1446  35011  bnj1467  35020  indexa  37712  sdclem1  37722  sbcalf  38093  sbcexf  38094  sbccomieg  42766  rexrabdioph  42767  or2expropbilem2  47018  or2expropbi  47019  ich2exprop  47456  ichnreuop  47457  reuopreuprim  47511