Theorem ifhvhv0 27879

Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0_ℎ) ∈ ℋ (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)

Assertion

Ref	Expression
ifhvhv0	⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Proof of Theorem ifhvhv0

Step	Hyp	Ref	Expression
1		ax-hv0cl 27860	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4150	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 1990  ifcif 4086   ℋchil 27776  0_ℎc0v 27781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-hv0cl 27860

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  hvsubsub4  27917  hvnegdi  27924  hvsubeq0  27925  hvaddcan  27927  hvsubadd  27934  normlem9at  27978  normsq  27991  normsub0  27993  norm-ii  27995  norm-iii  27997  normsub  28000  normpyth  28002  norm3dif  28007  norm3lemt  28009  norm3adifi  28010  normpar  28012  polid  28016  bcs  28038  pjoc1  28293  pjoc2  28298  h1de2ci  28415  spansn  28418  elspansn  28425  elspansn2  28426  h1datom  28441  spansnj  28506  spansncv  28512  pjch1  28529  pjadji  28544  pjaddi  28545  pjinormi  28546  pjsubi  28547  pjmuli  28548  pjcjt2  28551  pjch  28553  pjopyth  28579  pjnorm  28583  pjpyth  28584  pjnel  28585  eigre  28694  eigorth  28697  lnopeq0lem2  28865  lnopunii  28871  lnophmi  28877  pjss2coi  29023  pjssmi  29024  pjssge0i  29025  pjdifnormi  29026