Theorem elimel 4598

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.)

Hypothesis

Ref	Expression
elimel.1	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
elimel	⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 2822	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2822	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4594	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2107  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  fprg  7153  orduninsuc  7832  oawordeu  8555  oeoa  8597  omopth  8661  unfilem3  9312  inar1  10770  supsr  11107  renegcl  11523  peano5uzti  12652  eluzaddOLD  12857  eluzsubOLD  12858  ltweuz  13926  uzenom  13929  seqfn  13978  seq1  13979  seqp1  13981  sqeqor  14180  binom2  14181  nn0opth2  14232  faclbnd4lem2  14254  hashxp  14394  dvdsle  16253  divalglem7  16342  divalg  16346  gcdaddm  16466  smadiadetr  22177  iblcnlem  25306  ax5seglem8  28225  elimnv  29967  elimnvu  29968  nmlno0i  30078  nmblolbi  30084  blocn  30091  elimphu  30105  ubth  30157  htth  30202  ifhvhv0  30306  normlem6  30399  norm-iii  30424  norm3lemt  30436  ifchhv  30528  hhssablo  30547  hhssnvt  30549  shscl  30602  shslej  30664  shincl  30665  omlsii  30687  pjoml  30720  pjoc2  30723  chm0  30775  chne0  30778  chocin  30779  chj0  30781  chlejb1  30796  chnle  30798  ledi  30824  h1datom  30866  cmbr3  30892  pjoml2  30895  cmcm  30898  cmcm3  30899  lecm  30901  pjmuli  30973  pjige0  30975  pjhfo  30990  pj11  30998  eigre  31119  eigorth  31122  hoddi  31274  nmlnop0  31282  lnopeq  31293  lnopunilem2  31295  nmbdoplb  31309  nmcopex  31313  nmcoplb  31314  lnopcon  31319  lnfn0  31331  lnfnmul  31332  nmcfnex  31337  nmcfnlb  31338  lnfncon  31340  riesz4  31348  riesz1  31349  cnlnadjeu  31362  pjhmop  31434  pjidmco  31465  mdslmd1lem3  31611  mdslmd1lem4  31612  csmdsymi  31618  hatomic  31644  atord  31672  atcvat2  31673  bnj941  33814  bnj944  33980  kur14  34238  abs2sqle  34696  abs2sqlt  34697  onsucconn  35371  onsucsuccmp  35377  sdclem1  36659  mnurnd  43090  bnd2d  47774