Theorem nfsbcw 3733

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3736 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 1808	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3732	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-sbc 3712

This theorem is referenced by:  opelopabgf  5446  opelopabf  5451  ralrnmptw  6952  elovmporab  7493  elovmporab1w  7494  ovmpt3rabdm  7506  elovmpt3rab1  7507  dfopab2  7865  dfoprab3s  7866  mpoxopoveq  8006  elmptrab  22886  bnj1445  32924  bnj1446  32925  bnj1467  32934  ralxpes  33581  ralxp3es  33591  frpoins3xpg  33714  frpoins3xp3g  33715  indexa  35818  sdclem1  35828  sbcalf  36199  sbcexf  36200  sbccomieg  40531  rexrabdioph  40532  or2expropbilem2  44414  or2expropbi  44415  ich2exprop  44811  ichnreuop  44812  reuopreuprim  44866