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	|- 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		ax-1	|- ( [_ z / x ]_ C = y -> ( y e. A -> [_ z / x ]_ C = y ) )
9	7 8	simplbiim	|- ( z e. { x e. B | C = y } -> ( y e. A -> [_ z / x ]_ C = y ) )
10	9	impcom	|- ( ( y e. A /\ z e. { x e. B | C = y } ) -> [_ z / x ]_ C = y )
11	10	rgen2	|- A. y e. A A. z e. { x e. B | C = y } [_ z / x ]_ C = y
12		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 } )
13	11 12	ax-mp	|- Disj_ y e. A { x e. B | C = y }