Theorem nfcsbw 3934

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3935 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2374. (Revised by GG, 10-Jan-2024.)

Hypotheses

Ref	Expression
nfcsbw.1	⊢ Ⅎ𝑥𝐴
nfcsbw.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcsbw	⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfcsbw

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-csb 3908	. . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}
2		nftru 1800	. . . 4 ⊢ Ⅎ𝑧⊤
3		nftru 1800	. . . . 5 ⊢ Ⅎ𝑦⊤
4		nfcsbw.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴)
6		nfcsbw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
7	6	a1i 11	. . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵)
8	7	nfcrd 2896	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3811	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 2924	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2901	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1543	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1537   ∈ wcel 2105  {cab 2711  Ⅎwnfc 2887  [wsbc 3790  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-sbc 3791  df-csb 3908

This theorem is referenced by:  cbvrabcsfw  3951  elfvmptrab1w  7042  fmptcof  7149  fvmpopr2d  7594  elovmporab1w  7679  mpomptsx  8087  dmmpossx  8089  fmpox  8090  el2mpocsbcl  8108  fmpoco  8118  dfmpo  8125  mpocurryd  8292  fvmpocurryd  8294  nfsum  15723  fsum2dlem  15802  fsumcom2  15806  nfcprod  15941  fprod2dlem  16012  fprodcom2  16016  fsumcn  24907  fsum2cn  24908  dvmptfsum  26027  itgsubst  26104  iundisj2f  32609  f1od2  32738  esumiun  34074  poimirlem26  37632  cdlemkid  40918  cdlemk19x  40925  cdlemk11t  40928  fmpocos  42253  wdom2d2  43023  dmmpossx2  48181