Theorem ifhvhv0 28007

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

Syntax hints:   ∈ wcel 2030  ifcif 4119   ℋchil 27904  0_ℎc0v 27909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-hv0cl 27988

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  hvsubsub4  28045  hvnegdi  28052  hvsubeq0  28053  hvaddcan  28055  hvsubadd  28062  normlem9at  28106  normsq  28119  normsub0  28121  norm-ii  28123  norm-iii  28125  normsub  28128  normpyth  28130  norm3dif  28135  norm3lemt  28137  norm3adifi  28138  normpar  28140  polid  28144  bcs  28166  pjoc1  28421  pjoc2  28426  h1de2ci  28543  spansn  28546  elspansn  28553  elspansn2  28554  h1datom  28569  spansnj  28634  spansncv  28640  pjch1  28657  pjadji  28672  pjaddi  28673  pjinormi  28674  pjsubi  28675  pjmuli  28676  pjcjt2  28679  pjch  28681  pjopyth  28707  pjnorm  28711  pjpyth  28712  pjnel  28713  eigre  28822  eigorth  28825  lnopeq0lem2  28993  lnopunii  28999  lnophmi  29005  pjss2coi  29151  pjssmi  29152  pjssge0i  29153  pjdifnormi  29154