Theorem nfcsbw 3864

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3865 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 3839	. . 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 3750	. . . 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 3729  ⦋csb 3838

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 3730  df-csb 3839

This theorem is referenced by:  cbvrabcsfw  3879  elfvmptrab1w  6967  fmptcof  7075  fvmpopr2d  7520  elovmporab1w  7605  mpomptsx  8008  dmmpossx  8010  fmpox  8011  el2mpocsbcl  8026  fmpoco  8036  dfmpo  8043  mpocurryd  8210  fvmpocurryd  8212  nfsum  15615  fsum2dlem  15694  fsumcom2  15698  nfcprod  15833  fprod2dlem  15904  fprodcom2  15908  fsumcn  24815  fsum2cn  24816  dvmptfsum  25920  itgsubst  25997  iundisj2f  32649  f1od2  32781  esumiun  34244  poimirlem26  37958  cdlemkid  41373  cdlemk19x  41380  cdlemk11t  41383  fmpocos  42667  wdom2d2  43466  dmmpossx2  48771