Theorem ifhvhv0 31113

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

Syntax hints:   ∈ wcel 2114  ifcif 4467   ℋchba 31010  0_ℎc0v 31015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-hv0cl 31094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  hvsubsub4  31151  hvnegdi  31158  hvsubeq0  31159  hvaddcan  31161  hvsubadd  31168  normlem9at  31212  normsq  31225  normsub0  31227  norm-ii  31229  norm-iii  31231  normsub  31234  normpyth  31236  norm3dif  31241  norm3lemt  31243  norm3adifi  31244  normpar  31246  polid  31250  bcs  31272  pjoc1  31525  pjoc2  31530  h1de2ci  31647  spansn  31650  elspansn  31657  elspansn2  31658  h1datom  31673  spansnj  31738  spansncv  31744  pjch1  31761  pjadji  31776  pjaddi  31777  pjinormi  31778  pjsubi  31779  pjmuli  31780  pjcjt2  31783  pjch  31785  pjopyth  31811  pjnorm  31815  pjpyth  31816  pjnel  31817  eigre  31926  eigorth  31929  lnopeq0lem2  32097  lnopunii  32103  lnophmi  32109  pjss2coi  32255  pjssmi  32256  pjssge0i  32257  pjdifnormi  32258