Theorem nfsbcw 3760

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3739

This theorem is used by:  opelopabgf  5514  opelopabf  5519  ralrnmptw  7094  elovmporab  7667  elovmporab1w  7668  ovmpt3rabdm  7680  elovmpt3rab1  7681  dfopab2  8063  dfoprab3s  8064  ralxpes  8153  ralxp3es  8156  frpoins3xpg  8157  frpoins3xp3g  8158  mpoxopoveq  8237  elmptrab  24147  bnj1445  35717  bnj1446  35718  bnj1467  35727  indexa  38743  sdclem1  38753  sbcalf  39122  sbcexf  39123  sbccomieg  43876  rexrabdioph  43877  or2expropbilem2  48179  or2expropbi  48180  ich2exprop  48629  ichnreuop  48630  reuopreuprim  48684