Theorem nfcsbw 3920

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3921 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Mario Carneiro, 12-Oct-2016.) Avoid ax-13 2371. (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 3894	. . 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 2892	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3798	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 2926	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2902	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1548	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1542   ∈ wcel 2106  {cab 2709  Ⅎwnfc 2883  [wsbc 3777  ⦋csb 3893

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-sbc 3778  df-csb 3894

This theorem is referenced by:  cbvrabcsfw  3937  elfvmptrab1w  7024  fmptcof  7130  fvmpopr2d  7571  elovmporab1w  7655  mpomptsx  8052  dmmpossx  8054  fmpox  8055  el2mpocsbcl  8073  fmpoco  8083  dfmpo  8090  mpocurryd  8256  fvmpocurryd  8258  nfsum  15641  fsum2dlem  15720  fsumcom2  15724  nfcprod  15859  fprod2dlem  15928  fprodcom2  15932  fsumcn  24608  fsum2cn  24609  dvmptfsum  25716  itgsubst  25790  iundisj2f  32076  f1od2  32201  esumiun  33378  poimirlem26  36817  cdlemkid  40110  cdlemk19x  40117  cdlemk11t  40120  fmpocos  41362  wdom2d2  42076  dmmpossx2  47101