Theorem nfsbcw 3794

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2961  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sbc 3773

This theorem is referenced by:  opelopabgf  5427  opelopabf  5432  ralrnmptw  6860  elovmporab  7391  elovmporab1w  7392  ovmpt3rabdm  7404  elovmpt3rab1  7405  dfopab2  7750  dfoprab3s  7751  mpoxopoveq  7885  elmptrab  22435  bnj1445  32316  bnj1446  32317  bnj1467  32326  indexa  35023  sdclem1  35033  sbcalf  35407  sbcexf  35408  sbccomieg  39439  rexrabdioph  39440  or2expropbilem2  43317  or2expropbi  43318  ich2exprop  43682  ichnreuop  43683  reuopreuprim  43737