Theorem nfsbcw 3752

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

Syntax hints:  ⊤wtru 1548  Ⅎwnf 1790  Ⅎwnfc 2887  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-sbc 3731

This theorem is referenced by:  opelopabgf  5489  opelopabf  5494  ralrnmptw  7042  elovmporab  7609  elovmporab1w  7610  ovmpt3rabdm  7622  elovmpt3rab1  7623  dfopab2  8001  dfoprab3s  8002  ralxpes  8083  ralxp3es  8086  frpoins3xpg  8087  frpoins3xp3g  8088  mpoxopoveq  8166  elmptrab  23817  bnj1445  35233  bnj1446  35234  bnj1467  35243  indexa  38101  sdclem1  38111  sbcalf  38482  sbcexf  38483  sbccomieg  43239  rexrabdioph  43240  or2expropbilem2  47497  or2expropbi  47498  ich2exprop  47947  ichnreuop  47948  reuopreuprim  48002