Theorem nfsbcw 3812

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

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1779  Ⅎwnfc 2887  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-sbc 3791

This theorem is referenced by:  opelopabgf  5549  opelopabf  5554  ralrnmptw  7113  elovmporab  7678  elovmporab1w  7679  ovmpt3rabdm  7691  elovmpt3rab1  7692  dfopab2  8075  dfoprab3s  8076  ralxpes  8159  ralxp3es  8162  frpoins3xpg  8163  frpoins3xp3g  8164  mpoxopoveq  8242  elmptrab  23850  bnj1445  35036  bnj1446  35037  bnj1467  35046  indexa  37719  sdclem1  37729  sbcalf  38100  sbcexf  38101  sbccomieg  42780  rexrabdioph  42781  or2expropbilem2  46982  or2expropbi  46983  ich2exprop  47395  ichnreuop  47396  reuopreuprim  47450