This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }