Theorem nfsbcw 3826

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781  Ⅎwnfc 2893  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-sbc 3805

This theorem is referenced by:  opelopabgf  5559  opelopabf  5564  ralrnmptw  7128  elovmporab  7696  elovmporab1w  7697  ovmpt3rabdm  7709  elovmpt3rab1  7710  dfopab2  8093  dfoprab3s  8094  ralxpes  8177  ralxp3es  8180  frpoins3xpg  8181  frpoins3xp3g  8182  mpoxopoveq  8260  elmptrab  23856  bnj1445  35020  bnj1446  35021  bnj1467  35030  indexa  37693  sdclem1  37703  sbcalf  38074  sbcexf  38075  sbccomieg  42749  rexrabdioph  42750  or2expropbilem2  46948  or2expropbi  46949  ich2exprop  47345  ichnreuop  47346  reuopreuprim  47400