Theorem nfsbcw 3796

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

Syntax hints:  ⊤wtru 1535  Ⅎwnf 1778  Ⅎwnfc 2878  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-sbc 3775

This theorem is referenced by:  opelopabgf  5536  opelopabf  5541  ralrnmptw  7098  elovmporab  7661  elovmporab1w  7662  ovmpt3rabdm  7674  elovmpt3rab1  7675  dfopab2  8050  dfoprab3s  8051  ralxpes  8135  ralxp3es  8138  frpoins3xpg  8139  frpoins3xp3g  8140  mpoxopoveq  8218  elmptrab  23718  bnj1445  34611  bnj1446  34612  bnj1467  34621  indexa  37141  sdclem1  37151  sbcalf  37522  sbcexf  37523  sbccomieg  42135  rexrabdioph  42136  or2expropbilem2  46338  or2expropbi  46339  ich2exprop  46734  ichnreuop  46735  reuopreuprim  46789