Theorem ifhvhv0 30852

Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0_ℎ) ∈ ℋ. (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 30833	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4601	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 2098  ifcif 4532   ℋchba 30749  0_ℎc0v 30754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-hv0cl 30833

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4533

This theorem is referenced by:  hvsubsub4  30890  hvnegdi  30897  hvsubeq0  30898  hvaddcan  30900  hvsubadd  30907  normlem9at  30951  normsq  30964  normsub0  30966  norm-ii  30968  norm-iii  30970  normsub  30973  normpyth  30975  norm3dif  30980  norm3lemt  30982  norm3adifi  30983  normpar  30985  polid  30989  bcs  31011  pjoc1  31264  pjoc2  31269  h1de2ci  31386  spansn  31389  elspansn  31396  elspansn2  31397  h1datom  31412  spansnj  31477  spansncv  31483  pjch1  31500  pjadji  31515  pjaddi  31516  pjinormi  31517  pjsubi  31518  pjmuli  31519  pjcjt2  31522  pjch  31524  pjopyth  31550  pjnorm  31554  pjpyth  31555  pjnel  31556  eigre  31665  eigorth  31668  lnopeq0lem2  31836  lnopunii  31842  lnophmi  31848  pjss2coi  31994  pjssmi  31995  pjssge0i  31996  pjdifnormi  31997