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

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		ax-1	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 → ( 𝑦 ∈ 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 ) )
9	7 8	simplbiim	⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } → ( 𝑦 ∈ 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 ) )
10	9	impcom	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 )
11	10	rgen2	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦
12		invdisj	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } ⦋ 𝑧 / 𝑥 ⦌ 𝐶 = 𝑦 → Disj 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 } )
13	11 12	ax-mp	⊢ Disj 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐵 ∣ 𝐶 = 𝑦 }