Theorem infex 9456

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 23	. . 3 ⊢ (𝑅 Or 𝐴 → 𝑅 Or 𝐴)
3	2	infexd 9445	. 2 ⊢ (𝑅 Or 𝐴 → inf(𝐵, 𝐴, 𝑅) ∈ V)
4	1, 3	ax-mp 5	1 ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455   Or wor 5570  infcinf 9402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-po 5571  df-so 5572  df-cnv 5671  df-sup 9403  df-inf 9404

This theorem is referenced by:  limsupval  15527  lcmval  16651  odzval  16852  ramval  17069  imasdsfn  17569  imasdsval  17570  odval  19605  odf  19608  gexval  19649  nmoval  24853  metdsval  24986  ovolval  25613  ovolf  25622  elqaalem1  26461  elqaalem3  26463  ballotlemi  34869  pellfundval  43587  dgraaval  43851  dgraaf  43854  liminfgval  46456  liminfval2  46462  ovnval2  47239  finfdm2  47541