Theorem nfsbcw 3810

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2890  [wsbc 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-sbc 3789

This theorem is referenced by:  opelopabgf  5545  opelopabf  5550  ralrnmptw  7114  elovmporab  7679  elovmporab1w  7680  ovmpt3rabdm  7692  elovmpt3rab1  7693  dfopab2  8077  dfoprab3s  8078  ralxpes  8161  ralxp3es  8164  frpoins3xpg  8165  frpoins3xp3g  8166  mpoxopoveq  8244  elmptrab  23835  bnj1445  35058  bnj1446  35059  bnj1467  35068  indexa  37740  sdclem1  37750  sbcalf  38121  sbcexf  38122  sbccomieg  42804  rexrabdioph  42805  or2expropbilem2  47045  or2expropbi  47046  ich2exprop  47458  ichnreuop  47459  reuopreuprim  47513