Theorem infex

Description: An infimum is a set. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Hypothesis	infex.1	|- R Or A
Assertion	infex	|- inf ( B , A , R ) e. _V

Proof

Step	Hyp	Ref	Expression
1		infex.1	|- R Or A
2		id	|- ( R Or A -> R Or A )
3	2	infexd	|- ( R Or A -> inf ( B , A , R ) e. _V )
4	1 3	ax-mp	|- inf ( B , A , R ) e. _V