Theorem nfsbcw 3764

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2909  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-sbc 3743

This theorem is used by:  opelopabgf  5523  opelopabf  5528  ralrnmptw  7090  elovmporab  7663  elovmporab1w  7664  ovmpt3rabdm  7676  elovmpt3rab1  7677  dfopab2  8052  dfoprab3s  8053  ralxpes  8137  ralxp3es  8140  frpoins3xpg  8141  frpoins3xp3g  8142  mpoxopoveq  8220  elmptrab  24057  bnj1445  35555  bnj1446  35556  bnj1467  35565  indexa  38485  sdclem1  38495  sbcalf  38864  sbcexf  38865  sbccomieg  43636  rexrabdioph  43637  or2expropbilem2  47923  or2expropbi  47924  ich2exprop  48373  ichnreuop  48374  reuopreuprim  48428