Theorem ifhvhv0 31504

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

This proof depends on syntax axioms:   ∈ wcel 2145  ifcif 4485   ℋchba 31401  0_ℎc0v 31406

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-hv0cl 31485

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  hvsubsub4  31542  hvnegdi  31549  hvsubeq0  31550  hvaddcan  31552  hvsubadd  31559  normlem9at  31603  normsq  31616  normsub0  31618  norm-ii  31620  norm-iii  31622  normsub  31625  normpyth  31627  norm3dif  31632  norm3lemt  31634  norm3adifi  31635  normpar  31637  polid  31641  bcs  31663  pjoc1  31916  pjoc2  31921  h1de2ci  32038  spansn  32041  elspansn  32048  elspansn2  32049  h1datom  32064  spansnj  32129  spansncv  32135  pjch1  32152  pjadji  32167  pjaddi  32168  pjinormi  32169  pjsubi  32170  pjmuli  32171  pjcjt2  32174  pjch  32176  pjopyth  32202  pjnorm  32206  pjpyth  32207  pjnel  32208  eigre  32317  eigorth  32320  lnopeq0lem2  32488  lnopunii  32494  lnophmi  32500  pjss2coi  32646  pjssmi  32647  pjssge0i  32648  pjdifnormi  32649