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	abbi2i	⊢ ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) ) = { 𝑥 ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }
20	1 19	eqtr4i	⊢ ∩ 𝐴 = ( V ∖ ( ◡ ( V ∖ E ) “ 𝐴 ) )