Theorem nfsbcw 3738

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3741 with a disjoint variable condition, which does not require ax-13 2372. (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 1807	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3737	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786  Ⅎwnfc 2887  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-sbc 3717

This theorem is referenced by:  opelopabgf  5453  opelopabf  5458  ralrnmptw  6970  elovmporab  7515  elovmporab1w  7516  ovmpt3rabdm  7528  elovmpt3rab1  7529  dfopab2  7892  dfoprab3s  7893  mpoxopoveq  8035  elmptrab  22978  bnj1445  33024  bnj1446  33025  bnj1467  33034  ralxpes  33678  ralxp3es  33688  frpoins3xpg  33787  frpoins3xp3g  33788  indexa  35891  sdclem1  35901  sbcalf  36272  sbcexf  36273  sbccomieg  40615  rexrabdioph  40616  or2expropbilem2  44527  or2expropbi  44528  ich2exprop  44923  ichnreuop  44924  reuopreuprim  44978