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 ∈ A x ∈ B | C = y

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ _ x z
2 nfcv ⊢ Ⅎ _ x B
3 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ C
4 3 nfeq1 ⊢ Ⅎ 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 ∈ x ∈ B | C = y ↔ z ∈ B ∧ ⦋ z / x⦌ C = y
8 simprr ⊢ y ∈ A ∧ z ∈ B ∧ ⦋ z / x⦌ C = y → ⦋ z / x⦌ C = y
9 7 8 sylan2b ⊢ y ∈ A ∧ z ∈ x ∈ B | C = y → ⦋ z / x⦌ C = y
10 9 rgen2 ⊢ ∀ y ∈ A ∀ z ∈ x ∈ B | C = y ⦋ z / x⦌ C = y
11 invdisj ⊢ ∀ y ∈ A ∀ z ∈ x ∈ B | C = y ⦋ z / x⦌ C = y → Disj y ∈ A x ∈ B | C = y
12 10 11 ax-mp ⊢ Disj y ∈ A x ∈ B | C = y