Theorem nfcsbw 3912

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3913 with a disjoint variable condition, which does not require ax-13 2363. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2363. (Revised by Gino Giotto, 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 3886	. . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}
2		nftru 1798	. . . 4 ⊢ Ⅎ𝑧⊤
3		nftru 1798	. . . . 5 ⊢ Ⅎ𝑦⊤
4		nfcsbw.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴)
6		nfcsbw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
7	6	a1i 11	. . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵)
8	7	nfcrd 2884	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3790	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 2918	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2894	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1540	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1534   ∈ wcel 2098  {cab 2701  Ⅎwnfc 2875  [wsbc 3769  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-sbc 3770  df-csb 3886

This theorem is referenced by:  cbvrabcsfw  3929  elfvmptrab1w  7014  fmptcof  7120  fvmpopr2d  7562  elovmporab1w  7646  mpomptsx  8043  dmmpossx  8045  fmpox  8046  el2mpocsbcl  8065  fmpoco  8075  dfmpo  8082  mpocurryd  8249  fvmpocurryd  8251  nfsum  15633  fsum2dlem  15712  fsumcom2  15716  nfcprod  15851  fprod2dlem  15920  fprodcom2  15924  fsumcn  24709  fsum2cn  24710  dvmptfsum  25828  itgsubst  25905  iundisj2f  32256  f1od2  32381  esumiun  33547  poimirlem26  36970  cdlemkid  40263  cdlemk19x  40270  cdlemk11t  40273  fmpocos  41515  wdom2d2  42229  dmmpossx2  47167