Metamath Proof Explorer

Theorem dfint3

Description: Quantifier-free definition of class intersection. (Contributed by Scott Fenton, 13-Apr-2018)

Ref Expression
Assertion dfint3 ⊢ ⋂ A = V ∖ V ∖ E -1 A

Proof

Step Hyp Ref Expression
1 dfint2 ⊢ ⋂ A = x | ∀ y ∈ A x ∈ y
2 ralnex ⊢ ∀ y ∈ A ¬ y V ∖ E -1 x ↔ ¬ ∃ y ∈ A y V ∖ E -1 x
3 vex ⊢ y ∈ V
4 vex ⊢ x ∈ V
5 3 4 brcnv ⊢ y V ∖ E -1 x ↔ x V ∖ E y
6 brv ⊢ x V y
7 brdif ⊢ x V ∖ E y ↔ x V y ∧ ¬ x E y
8 6 7 mpbiran ⊢ x V ∖ E y ↔ ¬ x E y
9 5 8 bitr2i ⊢ ¬ x E y ↔ y V ∖ E -1 x
10 9 con1bii ⊢ ¬ y V ∖ E -1 x ↔ x E y
11 epel ⊢ x E y ↔ x ∈ y
12 10 11 bitr2i ⊢ x ∈ y ↔ ¬ y V ∖ E -1 x
13 12 ralbii ⊢ ∀ y ∈ A x ∈ y ↔ ∀ y ∈ A ¬ y V ∖ E -1 x
14 eldif ⊢ x ∈ V ∖ V ∖ E -1 A ↔ x ∈ V ∧ ¬ x ∈ V ∖ E -1 A
15 4 14 mpbiran ⊢ x ∈ V ∖ V ∖ E -1 A ↔ ¬ x ∈ V ∖ E -1 A
16 4 elima ⊢ x ∈ V ∖ E -1 A ↔ ∃ y ∈ A y V ∖ E -1 x
17 15 16 xchbinx ⊢ x ∈ V ∖ V ∖ E -1 A ↔ ¬ ∃ y ∈ A y V ∖ E -1 x
18 2 13 17 3bitr4ri ⊢ x ∈ V ∖ V ∖ E -1 A ↔ ∀ y ∈ A x ∈ y
19 18 eqabi ⊢ V ∖ V ∖ E -1 A = x | ∀ y ∈ A x ∈ y
20 1 19 eqtr4i ⊢ ⋂ A = V ∖ V ∖ E -1 A