Theorem relintab

Description: Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020)

	Ref	Expression
Assertion	relintab	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) } )

Proof

Step	Hyp	Ref	Expression
1		cnvcnv	⊢ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ( ∩ { 𝑥 ∣ 𝜑 } ∩ ( V × V ) )
2		incom	⊢ ( ∩ { 𝑥 ∣ 𝜑 } ∩ ( V × V ) ) = ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } )
3	1 2	eqtri	⊢ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } )
4		dfrel2	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } ↔ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑥 ∣ 𝜑 } )
5	4	biimpi	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑥 ∣ 𝜑 } )
6		relintabex	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ∃ 𝑥 𝜑 )
7	6	xpinintabd	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } ) = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ∧ 𝜑 ) } )
8		incom	⊢ ( ( V × V ) ∩ 𝑥 ) = ( 𝑥 ∩ ( V × V ) )
9		cnvcnv	⊢ ◡ ◡ 𝑥 = ( 𝑥 ∩ ( V × V ) )
10	8 9	eqtr4i	⊢ ( ( V × V ) ∩ 𝑥 ) = ◡ ◡ 𝑥
11	10	eqeq2i	⊢ ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ↔ 𝑤 = ◡ ◡ 𝑥 )
12	11	anbi1i	⊢ ( ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ∧ 𝜑 ) ↔ ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) )
13	12	exbii	⊢ ( ∃ 𝑥 ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) )
14	13	rabbii	⊢ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ∧ 𝜑 ) } = { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) }
15	14	inteqi	⊢ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ( ( V × V ) ∩ 𝑥 ) ∧ 𝜑 ) } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) }
16	7 15	eqtrdi	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } ) = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) } )
17	3 5 16	3eqtr3a	⊢ ( Rel ∩ { 𝑥 ∣ 𝜑 } → ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜑 ) } )