Theorem nfsbcw 3760

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2907  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3739

This theorem is used by:  opelopabgf  5511  opelopabf  5516  ralrnmptw  7082  elovmporab  7655  elovmporab1w  7656  ovmpt3rabdm  7668  elovmpt3rab1  7669  dfopab2  8046  dfoprab3s  8047  ralxpes  8131  ralxp3es  8134  frpoins3xpg  8135  frpoins3xp3g  8136  mpoxopoveq  8214  elmptrab  24108  bnj1445  35609  bnj1446  35610  bnj1467  35619  indexa  38587  sdclem1  38597  sbcalf  38966  sbcexf  38967  sbccomieg  43738  rexrabdioph  43739  or2expropbilem2  48025  or2expropbi  48026  ich2exprop  48475  ichnreuop  48476  reuopreuprim  48530