Theorem ifhvhv0 31008

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

Syntax hints:   ∈ wcel 2109  ifcif 4505   ℋchba 30905  0_ℎc0v 30910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-hv0cl 30989

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  hvsubsub4  31046  hvnegdi  31053  hvsubeq0  31054  hvaddcan  31056  hvsubadd  31063  normlem9at  31107  normsq  31120  normsub0  31122  norm-ii  31124  norm-iii  31126  normsub  31129  normpyth  31131  norm3dif  31136  norm3lemt  31138  norm3adifi  31139  normpar  31141  polid  31145  bcs  31167  pjoc1  31420  pjoc2  31425  h1de2ci  31542  spansn  31545  elspansn  31552  elspansn2  31553  h1datom  31568  spansnj  31633  spansncv  31639  pjch1  31656  pjadji  31671  pjaddi  31672  pjinormi  31673  pjsubi  31674  pjmuli  31675  pjcjt2  31678  pjch  31680  pjopyth  31706  pjnorm  31710  pjpyth  31711  pjnel  31712  eigre  31821  eigorth  31824  lnopeq0lem2  31992  lnopunii  31998  lnophmi  32004  pjss2coi  32150  pjssmi  32151  pjssge0i  32152  pjdifnormi  32153