Theorem brintclab

Description: Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020)

	Ref	Expression
Assertion	brintclab	|- ( A |^| { x | ph } B <-> A. x ( ph -> <. A , B >. e. x ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A |^| { x | ph } B <-> <. A , B >. e. |^| { x | ph } )
2		opex	|- <. A , B >. e. _V
3	2	elintab	|- ( <. A , B >. e. |^| { x | ph } <-> A. x ( ph -> <. A , B >. e. x ) )
4	1 3	bitri	|- ( A |^| { x | ph } B <-> A. x ( ph -> <. A , B >. e. x ) )