Theorem nfcsbw 3891

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

Syntax hints:  ⊤wtru 1541   ∈ wcel 2109  {cab 2708  Ⅎwnfc 2877  [wsbc 3756  ⦋csb 3865

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-sbc 3757  df-csb 3866

This theorem is referenced by:  cbvrabcsfw  3906  elfvmptrab1w  6998  fmptcof  7105  fvmpopr2d  7554  elovmporab1w  7639  mpomptsx  8046  dmmpossx  8048  fmpox  8049  el2mpocsbcl  8067  fmpoco  8077  dfmpo  8084  mpocurryd  8251  fvmpocurryd  8253  nfsum  15664  fsum2dlem  15743  fsumcom2  15747  nfcprod  15882  fprod2dlem  15953  fprodcom2  15957  fsumcn  24768  fsum2cn  24769  dvmptfsum  25886  itgsubst  25963  iundisj2f  32526  f1od2  32651  esumiun  34091  poimirlem26  37647  cdlemkid  40937  cdlemk19x  40944  cdlemk11t  40947  fmpocos  42229  wdom2d2  43031  dmmpossx2  48329