Theorem nfsbcw 3742

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3745 with a disjoint variable condition, which does not require ax-13 2379. (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 1806	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3741	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1545	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785  Ⅎwnfc 2936  [wsbc 3720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-sbc 3721

This theorem is referenced by:  opelopabgf  5392  opelopabf  5397  ralrnmptw  6837  elovmporab  7371  elovmporab1w  7372  ovmpt3rabdm  7384  elovmpt3rab1  7385  dfopab2  7732  dfoprab3s  7733  mpoxopoveq  7868  elmptrab  22432  bnj1445  32426  bnj1446  32427  bnj1467  32436  indexa  35171  sdclem1  35181  sbcalf  35552  sbcexf  35553  sbccomieg  39734  rexrabdioph  39735  or2expropbilem2  43625  or2expropbi  43626  ich2exprop  43988  ichnreuop  43989  reuopreuprim  44043