Theorem invdisjrab

Description: The restricted class abstractions { x e. B | C = y } for distinct y e. A are disjoint. (Contributed by AV, 6-May-2020) (Proof shortened by GG, 26-Jan-2024)

	Ref	Expression
Assertion	invdisjrab	$$⊢\underset{y\in A}{Disj}\left\{x\in B|C=y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
3		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌C$$
4	3	nfeq1	$$⊢Ⅎx⦋z/x⦌C=y$$
5		csbeq1a	$$⊢x=z\to C=⦋z/x⦌C$$
6	5	eqeq1d	$$⊢x=z\to \left(C=y\leftrightarrow ⦋z/x⦌C=y\right)$$
7	1 2 4 6	elrabf	$$⊢z\in \left\{x\in B|C=y\right\}\leftrightarrow \left(z\in B\wedge ⦋z/x⦌C=y\right)$$
8		simprr	$$⊢\left(y\in A\wedge \left(z\in B\wedge ⦋z/x⦌C=y\right)\right)\to ⦋z/x⦌C=y$$
9	7 8	sylan2b	$$⊢\left(y\in A\wedge z\in \left\{x\in B|C=y\right\}\right)\to ⦋z/x⦌C=y$$
10	9	rgen2	$$⊢\forall y\in A\forall z\in \left\{x\in B|C=y\right\}⦋z/x⦌C=y$$
11		invdisj	$$⊢\forall y\in A\forall z\in \left\{x\in B|C=y\right\}⦋z/x⦌C=y\to \underset{y\in A}{Disj}\left\{x\in B|C=y\right\}$$
12	10 11	ax-mp	$$⊢\underset{y\in A}{Disj}\left\{x\in B|C=y\right\}$$