Theorem nfcsbw 3869

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

Syntax hints:  ⊤wtru 1551   ∈ wcel 2132  {cab 2730  Ⅎwnfc 2899  [wsbc 3735  ⦋csb 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-sbc 3736  df-csb 3844

This theorem is referenced by:  cbvrabcsfw  3884  elfvmptrab1w  6988  fmptcof  7097  fvmpopr2d  7543  elovmporab1w  7628  mpomptsx  8030  dmmpossx  8032  fmpox  8033  el2mpocsbcl  8048  fmpoco  8058  dfmpo  8065  mpocurryd  8233  fvmpocurryd  8235  nfsum  15690  fsum2dlem  15769  fsumcom2  15773  nfcprod  15911  fprod2dlem  15982  fprodcom2  15986  fsumcn  24901  fsum2cn  24902  dvmptfsum  26006  itgsubst  26080  iundisj2f  32728  f1od2  32860  esumiun  34335  poimirlem26  38083  cdlemkid  41498  cdlemk19x  41505  cdlemk11t  41508  fmpocos  42790  wdom2d2  43550  dmmpossx2  48897