Theorem nfsbcw 3741

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1789  Ⅎwnfc 2888  [wsbc 3719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-sbc 3720

This theorem is referenced by:  opelopabgf  5454  opelopabf  5459  ralrnmptw  6964  elovmporab  7506  elovmporab1w  7507  ovmpt3rabdm  7519  elovmpt3rab1  7520  dfopab2  7878  dfoprab3s  7879  mpoxopoveq  8019  elmptrab  22959  bnj1445  33003  bnj1446  33004  bnj1467  33013  ralxpes  33657  ralxp3es  33667  frpoins3xpg  33766  frpoins3xp3g  33767  indexa  35870  sdclem1  35880  sbcalf  36251  sbcexf  36252  sbccomieg  40595  rexrabdioph  40596  or2expropbilem2  44478  or2expropbi  44479  ich2exprop  44875  ichnreuop  44876  reuopreuprim  44930