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 2402. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2402. (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 1832	. . 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 1575	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1569  Ⅎwnf 1811  Ⅎwnfc 2908  [wsbc 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3744

This theorem is referenced by:  opelopabgf  5525  opelopabf  5530  ralrnmptw  7089  elovmporab  7656  elovmporab1w  7657  ovmpt3rabdm  7669  elovmpt3rab1  7670  dfopab2  8048  dfoprab3s  8049  ralxpes  8131  ralxp3es  8134  frpoins3xpg  8135  frpoins3xp3g  8136  mpoxopoveq  8214  elmptrab  23963  bnj1445  35398  bnj1446  35399  bnj1467  35408  indexa  38350  sdclem1  38360  sbcalf  38731  sbcexf  38732  sbccomieg  43490  rexrabdioph  43491  or2expropbilem2  47737  or2expropbi  47738  ich2exprop  48187  ichnreuop  48188  reuopreuprim  48242