This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Disjointness df-disj
Description: A collection of classes B ( x ) is disjoint when for each element
y , it is in B ( x ) for at most one x . (Contributed by Mario Carneiro , 14-Nov-2016) (Revised by NM , 16-Jun-2017)
Ref
Expression
Assertion
df-disj ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
vx ⊢ 𝑥
1
cA ⊢ 𝐴
2
cB ⊢ 𝐵
3
0 1 2
wdisj ⊢ Disj 𝑥 ∈ 𝐴 𝐵
4
vy ⊢ 𝑦
5
4
cv ⊢ 𝑦
6
5 2
wcel ⊢ 𝑦 ∈ 𝐵
7
6 0 1
wrmo ⊢ ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
8
7 4
wal ⊢ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9
3 8
wb ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )