Theorem ifhvhv0 31054

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

Syntax hints:   ∈ wcel 2108  ifcif 4548   ℋchba 30951  0_ℎc0v 30956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-hv0cl 31035

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  hvsubsub4  31092  hvnegdi  31099  hvsubeq0  31100  hvaddcan  31102  hvsubadd  31109  normlem9at  31153  normsq  31166  normsub0  31168  norm-ii  31170  norm-iii  31172  normsub  31175  normpyth  31177  norm3dif  31182  norm3lemt  31184  norm3adifi  31185  normpar  31187  polid  31191  bcs  31213  pjoc1  31466  pjoc2  31471  h1de2ci  31588  spansn  31591  elspansn  31598  elspansn2  31599  h1datom  31614  spansnj  31679  spansncv  31685  pjch1  31702  pjadji  31717  pjaddi  31718  pjinormi  31719  pjsubi  31720  pjmuli  31721  pjcjt2  31724  pjch  31726  pjopyth  31752  pjnorm  31756  pjpyth  31757  pjnel  31758  eigre  31867  eigorth  31870  lnopeq0lem2  32038  lnopunii  32044  lnophmi  32050  pjss2coi  32196  pjssmi  32197  pjssge0i  32198  pjdifnormi  32199