Theorem ifhvhv0 31093

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

Syntax hints:   ∈ wcel 2114  ifcif 4467   ℋchba 30990  0_ℎc0v 30995

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 31074

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  31131  hvnegdi  31138  hvsubeq0  31139  hvaddcan  31141  hvsubadd  31148  normlem9at  31192  normsq  31205  normsub0  31207  norm-ii  31209  norm-iii  31211  normsub  31214  normpyth  31216  norm3dif  31221  norm3lemt  31223  norm3adifi  31224  normpar  31226  polid  31230  bcs  31252  pjoc1  31505  pjoc2  31510  h1de2ci  31627  spansn  31630  elspansn  31637  elspansn2  31638  h1datom  31653  spansnj  31718  spansncv  31724  pjch1  31741  pjadji  31756  pjaddi  31757  pjinormi  31758  pjsubi  31759  pjmuli  31760  pjcjt2  31763  pjch  31765  pjopyth  31791  pjnorm  31795  pjpyth  31796  pjnel  31797  eigre  31906  eigorth  31909  lnopeq0lem2  32077  lnopunii  32083  lnophmi  32089  pjss2coi  32235  pjssmi  32236  pjssge0i  32237  pjdifnormi  32238