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  6977  fmptcof  7084  fvmpopr2d  7531  elovmporab1w  7616  mpomptsx  8022  dmmpossx  8024  fmpox  8025  el2mpocsbcl  8041  fmpoco  8051  dfmpo  8058  mpocurryd  8225  fvmpocurryd  8227  nfsum  15633  fsum2dlem  15712  fsumcom2  15716  nfcprod  15851  fprod2dlem  15922  fprodcom2  15926  fsumcn  24794  fsum2cn  24795  dvmptfsum  25912  itgsubst  25989  iundisj2f  32569  f1od2  32694  esumiun  34077  poimirlem26  37633  cdlemkid  40923  cdlemk19x  40930  cdlemk11t  40933  fmpocos  42215  wdom2d2  43017  dmmpossx2  48318