Theorem nfsbcw 3765

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1812  Ⅎwnfc 2909  [wsbc 3743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-sbc 3744

This theorem is used by:  opelopabgf  5524  opelopabf  5529  ralrnmptw  7089  elovmporab  7658  elovmporab1w  7659  ovmpt3rabdm  7671  elovmpt3rab1  7672  dfopab2  8047  dfoprab3s  8048  ralxpes  8130  ralxp3es  8133  frpoins3xpg  8134  frpoins3xp3g  8135  mpoxopoveq  8213  elmptrab  23995  bnj1445  35441  bnj1446  35442  bnj1467  35451  indexa  38412  sdclem1  38422  sbcalf  38791  sbcexf  38792  sbccomieg  43548  rexrabdioph  43549  or2expropbilem2  47798  or2expropbi  47799  ich2exprop  48248  ichnreuop  48249  reuopreuprim  48303