Theorem nfcsbw 3879

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

Syntax hints:  ⊤wtru 1562   ∈ wcel 2143  {cab 2741  Ⅎwnfc 2910  [wsbc 3745  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-nf 1805  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-sbc 3746  df-csb 3854

This theorem is referenced by:  cbvrabcsfw  3894  elfvmptrab1w  7003  fmptcof  7112  fvmpopr2d  7558  elovmporab1w  7643  mpomptsx  8045  dmmpossx  8047  fmpox  8048  el2mpocsbcl  8064  fmpoco  8074  dfmpo  8081  mpocurryd  8249  fvmpocurryd  8251  nfsum  15728  fsum2dlem  15807  fsumcom2  15811  nfcprod  15949  fprod2dlem  16020  fprodcom2  16024  fsumcn  24939  fsum2cn  24940  dvmptfsum  26044  itgsubst  26118  iundisj2f  32796  f1od2  32927  esumiun  34393  poimirlem26  38150  cdlemkid  41565  cdlemk19x  41572  cdlemk11t  41575  fmpocos  42857  wdom2d2  43617  dmmpossx2  48950