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 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 }

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ 𝑥 𝑧
2 nfcv ⊢ Ⅎ 𝑥 𝐵
3 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐶
4 3 nfeq1 ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦
5 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐶 = ⦋ 𝑧 / 𝑥 ⦌ 𝐶 )
6 5 eqeq1d ⊢ ( 𝑥 = 𝑧 → ( 𝐶 = 𝑦 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 ) )
7 1 2 4 6 elrabf ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ↔ ( 𝑧 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 ) )
8 simprr ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 ) ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 )
9 7 8 sylan2b ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 )
10 9 rgen2 ⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦
11 invdisj ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 → Disj 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } )
12 10 11 ax-mp ⊢ Disj 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 }