Theorem nfcsbw 3905

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

Syntax hints:  ⊤wtru 1540   ∈ wcel 2107  {cab 2712  Ⅎwnfc 2882  [wsbc 3770  ⦋csb 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-sbc 3771  df-csb 3880

This theorem is referenced by:  cbvrabcsfw  3920  elfvmptrab1w  7023  fmptcof  7130  fvmpopr2d  7577  elovmporab1w  7662  mpomptsx  8071  dmmpossx  8073  fmpox  8074  el2mpocsbcl  8092  fmpoco  8102  dfmpo  8109  mpocurryd  8276  fvmpocurryd  8278  nfsum  15709  fsum2dlem  15788  fsumcom2  15792  nfcprod  15927  fprod2dlem  15998  fprodcom2  16002  fsumcn  24830  fsum2cn  24831  dvmptfsum  25949  itgsubst  26026  iundisj2f  32538  f1od2  32667  esumiun  34054  poimirlem26  37612  cdlemkid  40897  cdlemk19x  40904  cdlemk11t  40907  fmpocos  42233  wdom2d2  43010  dmmpossx2  48211