Theorem nfcsbw 3909

Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3910 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by Gino Giotto, 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 3884	. . 3 ⊢ ⦋𝐴 / 𝑦⦌𝐵 = {𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵}
2		nftru 1805	. . . 4 ⊢ Ⅎ𝑧⊤
3		nftru 1805	. . . . 5 ⊢ Ⅎ𝑦⊤
4		nfcsbw.1	. . . . . 6 ⊢ Ⅎ𝑥𝐴
5	4	a1i 11	. . . . 5 ⊢ (⊤ → Ⅎ𝑥𝐴)
6		nfcsbw.2	. . . . . . 7 ⊢ Ⅎ𝑥𝐵
7	6	a1i 11	. . . . . 6 ⊢ (⊤ → Ⅎ𝑥𝐵)
8	7	nfcrd 2969	. . . . 5 ⊢ (⊤ → Ⅎ𝑥 𝑧 ∈ 𝐵)
9	3, 5, 8	nfsbcdw 3793	. . . 4 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝑧 ∈ 𝐵)
10	2, 9	nfabdw 3000	. . 3 ⊢ (⊤ → Ⅎ𝑥{𝑧 ∣ [𝐴 / 𝑦]𝑧 ∈ 𝐵})
11	1, 10	nfcxfrd 2976	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
12	11	mptru 1544	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1538   ∈ wcel 2114  {cab 2799  Ⅎwnfc 2961  [wsbc 3772  ⦋csb 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sbc 3773  df-csb 3884

This theorem is referenced by:  cbvrabcsfw  3924  elfvmptrab1w  6794  fmptcof  6892  elovmporab1w  7392  mpomptsx  7762  dmmpossx  7764  fmpox  7765  el2mpocsbcl  7780  fmpoco  7790  dfmpo  7797  mpocurryd  7935  fvmpocurryd  7937  nfsumw  15047  fsum2dlem  15125  fsumcom2  15129  nfcprod  15265  fprod2dlem  15334  fprodcom2  15338  fsumcn  23478  fsum2cn  23479  dvmptfsum  24572  itgsubst  24646  iundisj2f  30340  f1od2  30457  esumiun  31353  poimirlem26  34933  cdlemkid  38087  cdlemk19x  38094  cdlemk11t  38097  wdom2d2  39681  dmmpossx2  44434