Theorem elimel 4555

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 2852	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2852	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4551	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

This proof depends on syntax axioms:   ∈ wcel 2147  ifcif 4485

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  fprg  7186  orduninsuc  7881  oawordeu  8594  oeoa  8637  omopth  8702  unfilem3  9330  bnd2d  9998  inar1  10890  supsr  11227  renegcl  11651  peano5uzti  12819  ltweuz  14134  uzenom  14137  seqfn  14186  seq1  14187  seqp1  14189  sqeqor  14390  binom2  14391  nn0opth2  14446  faclbnd4lem2  14468  hashxp  14609  dvdsle  16512  divalglem7  16601  divalg  16605  gcdaddm  16729  smadiadetr  23023  iblcnlem  26142  ax5seglem8  29547  elimnv  31318  elimnvu  31319  nmlno0i  31429  nmblolbi  31435  blocn  31442  elimphu  31456  ubth  31508  htth  31553  ifhvhv0  31657  normlem6  31750  norm-iii  31775  norm3lemt  31787  ifchhv  31879  hhssablo  31898  hhssnvt  31900  shscl  31953  shslej  32015  shincl  32016  omlsii  32038  pjoml  32071  pjoc2  32074  chm0  32126  chne0  32129  chocin  32130  chj0  32132  chlejb1  32147  chnle  32149  ledi  32175  h1datom  32217  cmbr3  32243  pjoml2  32246  cmcm  32249  cmcm3  32250  lecm  32252  pjmuli  32324  pjige0  32326  pjhfo  32341  pj11  32349  eigre  32470  eigorth  32473  hoddi  32625  nmlnop0  32633  lnopeq  32644  lnopunilem2  32646  nmbdoplb  32660  nmcopex  32664  nmcoplb  32665  lnopcon  32670  lnfn0  32682  lnfnmul  32683  nmcfnex  32688  nmcfnlb  32689  lnfncon  32691  riesz4  32699  riesz1  32700  cnlnadjeu  32713  pjhmop  32785  pjidmco  32816  mdslmd1lem3  32962  mdslmd1lem4  32963  csmdsymi  32969  hatomic  32995  atord  33023  atcvat2  33024  bnj941  35486  bnj944  35651  kur14  36161  abs2sqle  36625  abs2sqlt  36626  onsucconn  37417  onsucsuccmp  37423  sdclem1  38880  mnurnd  45470