Theorem elimel 4551

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

Syntax hints:   ∈ wcel 2114  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  fprg  7110  orduninsuc  7795  oawordeu  8492  oeoa  8535  omopth  8600  unfilem3  9219  inar1  10698  supsr  11035  renegcl  11456  peano5uzti  12594  ltweuz  13896  uzenom  13899  seqfn  13948  seq1  13949  seqp1  13951  sqeqor  14151  binom2  14152  nn0opth2  14207  faclbnd4lem2  14229  hashxp  14369  dvdsle  16249  divalglem7  16338  divalg  16342  gcdaddm  16464  smadiadetr  22631  iblcnlem  25758  ax5seglem8  29021  elimnv  30770  elimnvu  30771  nmlno0i  30881  nmblolbi  30887  blocn  30894  elimphu  30908  ubth  30960  htth  31005  ifhvhv0  31109  normlem6  31202  norm-iii  31227  norm3lemt  31239  ifchhv  31331  hhssablo  31350  hhssnvt  31352  shscl  31405  shslej  31467  shincl  31468  omlsii  31490  pjoml  31523  pjoc2  31526  chm0  31578  chne0  31581  chocin  31582  chj0  31584  chlejb1  31599  chnle  31601  ledi  31627  h1datom  31669  cmbr3  31695  pjoml2  31698  cmcm  31701  cmcm3  31702  lecm  31704  pjmuli  31776  pjige0  31778  pjhfo  31793  pj11  31801  eigre  31922  eigorth  31925  hoddi  32077  nmlnop0  32085  lnopeq  32096  lnopunilem2  32098  nmbdoplb  32112  nmcopex  32116  nmcoplb  32117  lnopcon  32122  lnfn0  32134  lnfnmul  32135  nmcfnex  32140  nmcfnlb  32141  lnfncon  32143  riesz4  32151  riesz1  32152  cnlnadjeu  32165  pjhmop  32237  pjidmco  32268  mdslmd1lem3  32414  mdslmd1lem4  32415  csmdsymi  32421  hatomic  32447  atord  32475  atcvat2  32476  bnj941  34948  bnj944  35113  kur14  35429  abs2sqle  35893  abs2sqlt  35894  onsucconn  36651  onsucsuccmp  36657  sdclem1  37991  mnurnd  44636  bnd2d  50037