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 2404. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2404. (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 2911  [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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-sbc 3743

This theorem is used by:  opelopabgf  5519  opelopabf  5524  ralrnmptw  7118  elovmporab  7691  elovmporab1w  7692  ovmpt3rabdm  7704  elovmpt3rab1  7705  dfopab2  8088  dfoprab3s  8089  ralxpes  8180  ralxp3es  8183  frpoins3xpg  8184  frpoins3xp3g  8185  mpoxopoveq  8264  elmptrab  24176  bnj1445  35744  bnj1446  35745  bnj1467  35754  indexa  38859  sdclem1  38869  sbcalf  39238  sbcexf  39239  sbccomieg  43993  rexrabdioph  43994  or2expropbilem2  48308  or2expropbi  48309  ich2exprop  48758  ichnreuop  48759  reuopreuprim  48813