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 𝐴 ↔ ∀ 𝑥 ∃* 𝑢𝐴 𝑥𝑢 )

Proof

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