Theorem infex 9543

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

Hypothesis

Ref	Expression
infex.1	⊢ 𝑅 Or 𝐴

Assertion

Ref	Expression
infex	⊢ inf(𝐵, 𝐴, 𝑅) ∈ V

Proof of Theorem infex

Step	Hyp	Ref	Expression
1		infex.1	. 2 ⊢ 𝑅 Or 𝐴
2		id 22	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Or 𝐴)
3	2	infexd 9533	. 2 ⊢ (𝑅 Or 𝐴 → inf(𝐵, 𝐴, 𝑅) ∈ V)
4	1, 3	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V

Syntax hints:   ∈ wcel 2100  Vcvv 3472   Or wor 5597  infcinf 9491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437  ax-un 7751

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-rmo 3373  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-po 5598  df-so 5599  df-cnv 5694  df-sup 9492  df-inf 9493

This theorem is referenced by:  limsupval  15497  lcmval  16614  odzval  16814  ramval  17031  imasdsfn  17550  imasdsval  17551  odval  19554  odf  19557  gexval  19598  nmoval  24746  metdsval  24877  ovolval  25516  ovolf  25525  elqaalem1  26370  elqaalem3  26372  ballotlemi  34372  pellfundval  42608  dgraaval  42876  dgraaf  42879  liminfgval  45453  liminfval2  45459  ovnval2  46236  finfdm2  46538