Theorem brlb

Description: Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018)

	Ref	Expression
Hypotheses	brub.1	|- S e. _V
	brub.2	|- A e. _V
Assertion	brlb	|- ( S LB R A <-> A. x e. S A R x )

Proof

Step	Hyp	Ref	Expression
1		brub.1	|- S e. _V
2		brub.2	|- A e. _V
3		df-lb	|- LB R = UB `' R
4	3	breqi	|- ( S LB R A <-> S UB `' R A )
5	1 2	brub	|- ( S UB `' R A <-> A. x e. S x `' R A )
6		vex	|- x e. _V
7	6 2	brcnv	|- ( x `' R A <-> A R x )
8	7	ralbii	|- ( A. x e. S x `' R A <-> A. x e. S A R x )
9	4 5 8	3bitri	|- ( S LB R A <-> A. x e. S A R x )