Theorem elimel 4100

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

Syntax hints:   ∈ wcel 1977  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  fprg  6327  orduninsuc  6935  oawordeu  7522  oeoa  7564  omopth  7625  unfilem3  8111  inar1  9476  supsr  9812  renegcl  10223  peano5uzti  11343  eluzadd  11592  eluzsub  11593  ltweuz  12622  uzenom  12625  seqfn  12675  seq1  12676  seqp1  12678  sqeqor  12840  binom2  12841  nn0opth2  12921  faclbnd4lem2  12943  hashxp  13081  dvdsle  14870  divalglem7  14960  divalg  14964  gcdaddm  15084  smadiadetr  20300  iblcnlem  23361  ax5seglem8  25616  elimnv  26922  elimnvu  26923  nmlno0i  27033  nmblolbi  27039  blocn  27046  elimphu  27060  ubth  27113  htth  27159  ifhvhv0  27263  normlem6  27356  norm-iii  27381  norm3lemt  27393  ifchhv  27485  hhssablo  27504  hhssnvt  27506  shscl  27561  shslej  27623  shincl  27624  omlsii  27646  pjoml  27679  pjoc2  27682  chm0  27734  chne0  27737  chocin  27738  chj0  27740  chlejb1  27755  chnle  27757  ledi  27783  h1datom  27825  cmbr3  27851  pjoml2  27854  cmcm  27857  cmcm3  27858  lecm  27860  pjmuli  27932  pjige0  27934  pjhfo  27949  pj11  27957  eigre  28078  eigorth  28081  hoddi  28233  nmlnop0  28241  lnopeq  28252  lnopunilem2  28254  nmbdoplb  28268  nmcopex  28272  nmcoplb  28273  lnopcon  28278  lnfn0  28290  lnfnmul  28291  nmcfnex  28296  nmcfnlb  28297  lnfncon  28299  riesz4  28307  riesz1  28308  cnlnadjeu  28321  pjhmop  28393  pjidmco  28424  mdslmd1lem3  28570  mdslmd1lem4  28571  csmdsymi  28577  hatomic  28603  atord  28631  atcvat2  28632  bnj941  30097  bnj944  30262  kur14  30452  abs2sqle  30828  abs2sqlt  30829  onsuccon  31607  onsucsuccmp  31613  sdclem1  32709  bnd2d  42226