Theorem nfcsbw 3876

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3877 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2377. (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 3851	. . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}
2		nftru 1806	. . . 4 ⊢ Ⅎ𝑧⊤
3		nftru 1806	. . . . 5 ⊢ Ⅎ𝑦⊤
4		nfcsbw.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴)
6		nfcsbw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
7	6	a1i 11	. . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵)
8	7	nfcrd 2893	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3762	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 2921	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2898	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1549	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1543   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  [wsbc 3741  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3742  df-csb 3851

This theorem is referenced by:  cbvrabcsfw  3891  elfvmptrab1w  6970  fmptcof  7077  fvmpopr2d  7522  elovmporab1w  7607  mpomptsx  8010  dmmpossx  8012  fmpox  8013  el2mpocsbcl  8029  fmpoco  8039  dfmpo  8046  mpocurryd  8213  fvmpocurryd  8215  nfsum  15618  fsum2dlem  15697  fsumcom2  15701  nfcprod  15836  fprod2dlem  15907  fprodcom2  15911  fsumcn  24821  fsum2cn  24822  dvmptfsum  25939  itgsubst  26016  iundisj2f  32647  f1od2  32779  esumiun  34232  poimirlem26  37818  cdlemkid  41233  cdlemk19x  41240  cdlemk11t  41243  fmpocos  42527  wdom2d2  43313  dmmpossx2  48619