Theorem elimel 4545

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

Syntax hints:   ∈ wcel 2111  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  fprg  7088  orduninsuc  7773  oawordeu  8470  oeoa  8512  omopth  8577  unfilem3  9191  inar1  10666  supsr  11003  renegcl  11424  peano5uzti  12563  eluzaddOLD  12767  eluzsubOLD  12768  ltweuz  13868  uzenom  13871  seqfn  13920  seq1  13921  seqp1  13923  sqeqor  14123  binom2  14124  nn0opth2  14179  faclbnd4lem2  14201  hashxp  14341  dvdsle  16221  divalglem7  16310  divalg  16314  gcdaddm  16436  smadiadetr  22591  iblcnlem  25718  ax5seglem8  28915  elimnv  30661  elimnvu  30662  nmlno0i  30772  nmblolbi  30778  blocn  30785  elimphu  30799  ubth  30851  htth  30896  ifhvhv0  31000  normlem6  31093  norm-iii  31118  norm3lemt  31130  ifchhv  31222  hhssablo  31241  hhssnvt  31243  shscl  31296  shslej  31358  shincl  31359  omlsii  31381  pjoml  31414  pjoc2  31417  chm0  31469  chne0  31472  chocin  31473  chj0  31475  chlejb1  31490  chnle  31492  ledi  31518  h1datom  31560  cmbr3  31586  pjoml2  31589  cmcm  31592  cmcm3  31593  lecm  31595  pjmuli  31667  pjige0  31669  pjhfo  31684  pj11  31692  eigre  31813  eigorth  31816  hoddi  31968  nmlnop0  31976  lnopeq  31987  lnopunilem2  31989  nmbdoplb  32003  nmcopex  32007  nmcoplb  32008  lnopcon  32013  lnfn0  32025  lnfnmul  32026  nmcfnex  32031  nmcfnlb  32032  lnfncon  32034  riesz4  32042  riesz1  32043  cnlnadjeu  32056  pjhmop  32128  pjidmco  32159  mdslmd1lem3  32305  mdslmd1lem4  32306  csmdsymi  32312  hatomic  32338  atord  32366  atcvat2  32367  bnj941  34782  bnj944  34948  kur14  35258  abs2sqle  35722  abs2sqlt  35723  onsucconn  36478  onsucsuccmp  36484  sdclem1  37789  mnurnd  44322  bnd2d  49719