Theorem ifhvhv0 31283

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

Syntax hints:   ∈ wcel 2145  ifcif 4483   ℋchba 31180  0_ℎc0v 31185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-hv0cl 31264

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  hvsubsub4  31321  hvnegdi  31328  hvsubeq0  31329  hvaddcan  31331  hvsubadd  31338  normlem9at  31382  normsq  31395  normsub0  31397  norm-ii  31399  norm-iii  31401  normsub  31404  normpyth  31406  norm3dif  31411  norm3lemt  31413  norm3adifi  31414  normpar  31416  polid  31420  bcs  31442  pjoc1  31695  pjoc2  31700  h1de2ci  31817  spansn  31820  elspansn  31827  elspansn2  31828  h1datom  31843  spansnj  31908  spansncv  31914  pjch1  31931  pjadji  31946  pjaddi  31947  pjinormi  31948  pjsubi  31949  pjmuli  31950  pjcjt2  31953  pjch  31955  pjopyth  31981  pjnorm  31985  pjpyth  31986  pjnel  31987  eigre  32096  eigorth  32099  lnopeq0lem2  32267  lnopunii  32273  lnophmi  32279  pjss2coi  32425  pjssmi  32426  pjssge0i  32427  pjdifnormi  32428