Theorem ifhvhv0 31013

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

Syntax hints:   ∈ wcel 2113  ifcif 4476   ℋchba 30910  0_ℎc0v 30915

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-hv0cl 30994

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  hvsubsub4  31051  hvnegdi  31058  hvsubeq0  31059  hvaddcan  31061  hvsubadd  31068  normlem9at  31112  normsq  31125  normsub0  31127  norm-ii  31129  norm-iii  31131  normsub  31134  normpyth  31136  norm3dif  31141  norm3lemt  31143  norm3adifi  31144  normpar  31146  polid  31150  bcs  31172  pjoc1  31425  pjoc2  31430  h1de2ci  31547  spansn  31550  elspansn  31557  elspansn2  31558  h1datom  31573  spansnj  31638  spansncv  31644  pjch1  31661  pjadji  31676  pjaddi  31677  pjinormi  31678  pjsubi  31679  pjmuli  31680  pjcjt2  31683  pjch  31685  pjopyth  31711  pjnorm  31715  pjpyth  31716  pjnel  31717  eigre  31826  eigorth  31829  lnopeq0lem2  31997  lnopunii  32003  lnophmi  32009  pjss2coi  32155  pjssmi  32156  pjssge0i  32157  pjdifnormi  32158