Theorem ifhvhv0 28799

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 28780	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4534	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 2114  ifcif 4467   ℋchba 28696  0_ℎc0v 28701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-hv0cl 28780

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  hvsubsub4  28837  hvnegdi  28844  hvsubeq0  28845  hvaddcan  28847  hvsubadd  28854  normlem9at  28898  normsq  28911  normsub0  28913  norm-ii  28915  norm-iii  28917  normsub  28920  normpyth  28922  norm3dif  28927  norm3lemt  28929  norm3adifi  28930  normpar  28932  polid  28936  bcs  28958  pjoc1  29211  pjoc2  29216  h1de2ci  29333  spansn  29336  elspansn  29343  elspansn2  29344  h1datom  29359  spansnj  29424  spansncv  29430  pjch1  29447  pjadji  29462  pjaddi  29463  pjinormi  29464  pjsubi  29465  pjmuli  29466  pjcjt2  29469  pjch  29471  pjopyth  29497  pjnorm  29501  pjpyth  29502  pjnel  29503  eigre  29612  eigorth  29615  lnopeq0lem2  29783  lnopunii  29789  lnophmi  29795  pjss2coi  29941  pjssmi  29942  pjssge0i  29943  pjdifnormi  29944