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)

	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		ax-1	$$⊢⦋z/x⦌C=y\to \left(y\in A\to ⦋z/x⦌C=y\right)$$
9	7 8	simplbiim	$$⊢z\in \left\{x\in B|C=y\right\}\to \left(y\in A\to ⦋z/x⦌C=y\right)$$
10	9	impcom	$$⊢\left(y\in A\wedge z\in \left\{x\in B|C=y\right\}\right)\to ⦋z/x⦌C=y$$
11	10	rgen2	$$⊢\forall y\in A\forall z\in \left\{x\in B|C=y\right\}⦋z/x⦌C=y$$
12		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\}$$
13	11 12	ax-mp	$$⊢\underset{y\in A}{Disj}\left\{x\in B|C=y\right\}$$