Theorem elimel 4549

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

Syntax hints:   ∈ wcel 2141  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4480

This theorem is referenced by:  fprg  7134  orduninsuc  7819  oawordeu  8519  oeoa  8562  omopth  8627  unfilem3  9247  inar1  10730  supsr  11067  renegcl  11491  peano5uzti  12660  ltweuz  13971  uzenom  13974  seqfn  14023  seq1  14024  seqp1  14026  sqeqor  14226  binom2  14227  nn0opth2  14282  faclbnd4lem2  14304  hashxp  14444  dvdsle  16327  divalglem7  16416  divalg  16420  gcdaddm  16542  smadiadetr  22715  iblcnlem  25831  ax5seglem8  29083  elimnv  30832  elimnvu  30833  nmlno0i  30943  nmblolbi  30949  blocn  30956  elimphu  30970  ubth  31022  htth  31067  ifhvhv0  31171  normlem6  31264  norm-iii  31289  norm3lemt  31301  ifchhv  31393  hhssablo  31412  hhssnvt  31414  shscl  31467  shslej  31529  shincl  31530  omlsii  31552  pjoml  31585  pjoc2  31588  chm0  31640  chne0  31643  chocin  31644  chj0  31646  chlejb1  31661  chnle  31663  ledi  31689  h1datom  31731  cmbr3  31757  pjoml2  31760  cmcm  31763  cmcm3  31764  lecm  31766  pjmuli  31838  pjige0  31840  pjhfo  31855  pj11  31863  eigre  31984  eigorth  31987  hoddi  32139  nmlnop0  32147  lnopeq  32158  lnopunilem2  32160  nmbdoplb  32174  nmcopex  32178  nmcoplb  32179  lnopcon  32184  lnfn0  32196  lnfnmul  32197  nmcfnex  32202  nmcfnlb  32203  lnfncon  32205  riesz4  32213  riesz1  32214  cnlnadjeu  32227  pjhmop  32299  pjidmco  32330  mdslmd1lem3  32476  mdslmd1lem4  32477  csmdsymi  32483  hatomic  32509  atord  32537  atcvat2  32538  bnj941  35032  bnj944  35197  kur14  35530  abs2sqle  35994  abs2sqlt  35995  onsucconn  36762  onsucsuccmp  36768  sdclem1  38206  mnurnd  44823  bnd2d  50266