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	|- Disj_ y e. A { x e. B | C = y }

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ x z
2		nfcv	|- F/_ x B
3		nfcsb1v	|- F/_ x [_ z / x ]_ C
4	3	nfeq1	|- F/ x [_ z / x ]_ C = y
5		csbeq1a	|- ( x = z -> C = [_ z / x ]_ C )
6	5	eqeq1d	|- ( x = z -> ( C = y <-> [_ z / x ]_ C = y ) )
7	1 2 4 6	elrabf	|- ( z e. { x e. B | C = y } <-> ( z e. B /\ [_ z / x ]_ C = y ) )
8		simprr	|- ( ( y e. A /\ ( z e. B /\ [_ z / x ]_ C = y ) ) -> [_ z / x ]_ C = y )
9	7 8	sylan2b	|- ( ( y e. A /\ z e. { x e. B | C = y } ) -> [_ z / x ]_ C = y )
10	9	rgen2	|- A. y e. A A. z e. { x e. B | C = y } [_ z / x ]_ C = y
11		invdisj	|- ( A. y e. A A. z e. { x e. B | C = y } [_ z / x ]_ C = y -> Disj_ y e. A { x e. B | C = y } )
12	10 11	ax-mp	|- Disj_ y e. A { x e. B | C = y }