This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfint3

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

Ref Expression
Assertion dfint3 ∩ 𝐴 = ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dfint2 ⊢ ∩ 𝐴 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }
2 ralnex ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ ( V ∖ E ) 𝑥 ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑦 ◡ ( V ∖ E ) 𝑥 )
3 vex ⊢ 𝑦 ∈ V
4 vex ⊢ 𝑥 ∈ V
5 3 4 brcnv ⊢ ( 𝑦 ◡ ( V ∖ E ) 𝑥 ↔ 𝑥 ( V ∖ E ) 𝑦 )
6 brv ⊢ 𝑥 V 𝑦
7 brdif ⊢ ( 𝑥 ( V ∖ E ) 𝑦 ↔ ( 𝑥 V 𝑦 ∧ ¬ 𝑥 E 𝑦 ) )
8 6 7 mpbiran ⊢ ( 𝑥 ( V ∖ E ) 𝑦 ↔ ¬ 𝑥 E 𝑦 )
9 5 8 bitr2i ⊢ ( ¬ 𝑥 E 𝑦 ↔ 𝑦 ◡ ( V ∖ E ) 𝑥 )
10 9 con1bii ⊢ ( ¬ 𝑦 ◡ ( V ∖ E ) 𝑥 ↔ 𝑥 E 𝑦 )
11 epel ⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
12 10 11 bitr2i ⊢ ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑦 ◡ ( V ∖ E ) 𝑥 )
13 12 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ ( V ∖ E ) 𝑥 )
14 eldif ⊢ ( 𝑥 ∈ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ ( ◡ ( V ∖ E ) “ 𝐴 ) ) )
15 4 14 mpbiran ⊢ ( 𝑥 ∈ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) ↔ ¬ 𝑥 ∈ ( ◡ ( V ∖ E ) “ 𝐴 ) )
16 4 elima ⊢ ( 𝑥 ∈ ( ◡ ( V ∖ E ) “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ◡ ( V ∖ E ) 𝑥 )
17 15 16 xchbinx ⊢ ( 𝑥 ∈ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) ↔ ¬ ∃ 𝑦 ∈ 𝐴 𝑦 ◡ ( V ∖ E ) 𝑥 )
18 2 13 17 3bitr4ri ⊢ ( 𝑥 ∈ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
19 18 eqabi ⊢ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }
20 1 19 eqtr4i ⊢ ∩ 𝐴 = ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) )