Theorem nfcsbw 3859

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3860 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 3834	. . 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 2891	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3746	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 2918	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2896	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1549	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1543   ∈ wcel 2114  {cab 2713  Ⅎwnfc 2882  [wsbc 3725  ⦋csb 3833

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 2184  ax-ext 2707

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 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-sbc 3726  df-csb 3834

This theorem is referenced by:  cbvrabcsfw  3874  elfvmptrab1w  6964  fmptcof  7072  fvmpopr2d  7518  elovmporab1w  7603  mpomptsx  8006  dmmpossx  8008  fmpox  8009  el2mpocsbcl  8024  fmpoco  8034  dfmpo  8041  mpocurryd  8208  fvmpocurryd  8210  nfsum  15642  fsum2dlem  15721  fsumcom2  15725  nfcprod  15863  fprod2dlem  15934  fprodcom2  15938  fsumcn  24825  fsum2cn  24826  dvmptfsum  25930  itgsubst  26004  iundisj2f  32648  f1od2  32780  esumiun  34226  poimirlem26  37955  cdlemkid  41370  cdlemk19x  41377  cdlemk11t  41380  fmpocos  42663  wdom2d2  43451  dmmpossx2  48801