Theorem nfsbcw 3800

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3803 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2369. (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 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 3799	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1546	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1783  Ⅎwnfc 2881  [wsbc 3778

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-sbc 3779

This theorem is referenced by:  opelopabgf  5541  opelopabf  5546  ralrnmptw  7096  elovmporab  7656  elovmporab1w  7657  ovmpt3rabdm  7669  elovmpt3rab1  7670  dfopab2  8042  dfoprab3s  8043  ralxpes  8126  ralxp3es  8129  frpoins3xpg  8130  frpoins3xp3g  8131  mpoxopoveq  8208  elmptrab  23553  bnj1445  34351  bnj1446  34352  bnj1467  34361  indexa  36906  sdclem1  36916  sbcalf  37287  sbcexf  37288  sbccomieg  41835  rexrabdioph  41836  or2expropbilem2  46043  or2expropbi  46044  ich2exprop  46439  ichnreuop  46440  reuopreuprim  46494