Metamath Proof Explorer

Theorem dfeldisj4

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj4 ⊢ ElDisj A ↔ ∀ x ∃* u ∈ A x ∈ u

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
2 relres ⊢ Rel ⁡ E -1 ↾ A
3 dfdisjALTV4 ⊢ Disj E -1 ↾ A ↔ ∀ x ∃* u u E -1 ↾ A x ∧ Rel ⁡ E -1 ↾ A
4 2 3 mpbiran2 ⊢ Disj E -1 ↾ A ↔ ∀ x ∃* u u E -1 ↾ A x
5 brcnvepres ⊢ u ∈ V ∧ x ∈ V → u E -1 ↾ A x ↔ u ∈ A ∧ x ∈ u
6 5 el2v ⊢ u E -1 ↾ A x ↔ u ∈ A ∧ x ∈ u
7 6 mobii ⊢ ∃* u u E -1 ↾ A x ↔ ∃* u u ∈ A ∧ x ∈ u
8 df-rmo ⊢ ∃* u ∈ A x ∈ u ↔ ∃* u u ∈ A ∧ x ∈ u
9 7 8 bitr4i ⊢ ∃* u u E -1 ↾ A x ↔ ∃* u ∈ A x ∈ u
10 9 albii ⊢ ∀ x ∃* u u E -1 ↾ A x ↔ ∀ x ∃* u ∈ A x ∈ u
11 1 4 10 3bitri ⊢ ElDisj A ↔ ∀ x ∃* u ∈ A x ∈ u