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