Theorem nfcsbw 3885

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

Syntax hints:  ⊤wtru 1541   ∈ wcel 2109  {cab 2707  Ⅎwnfc 2876  [wsbc 3750  ⦋csb 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-sbc 3751  df-csb 3860

This theorem is referenced by:  cbvrabcsfw  3900  elfvmptrab1w  6978  fmptcof  7085  fvmpopr2d  7532  elovmporab1w  7617  mpomptsx  8023  dmmpossx  8025  fmpox  8026  el2mpocsbcl  8042  fmpoco  8052  dfmpo  8059  mpocurryd  8226  fvmpocurryd  8228  nfsum  15635  fsum2dlem  15714  fsumcom2  15718  nfcprod  15853  fprod2dlem  15924  fprodcom2  15928  fsumcn  24796  fsum2cn  24797  dvmptfsum  25914  itgsubst  25991  iundisj2f  32571  f1od2  32696  esumiun  34079  poimirlem26  37635  cdlemkid  40925  cdlemk19x  40932  cdlemk11t  40935  fmpocos  42217  wdom2d2  43019  dmmpossx2  48320