Theorem elimel 4544

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

Syntax hints:   ∈ wcel 2113  ifcif 4474

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4475

This theorem is referenced by:  fprg  7094  orduninsuc  7779  oawordeu  8476  oeoa  8518  omopth  8583  unfilem3  9198  inar1  10673  supsr  11010  renegcl  11431  peano5uzti  12569  ltweuz  13870  uzenom  13873  seqfn  13922  seq1  13923  seqp1  13925  sqeqor  14125  binom2  14126  nn0opth2  14181  faclbnd4lem2  14203  hashxp  14343  dvdsle  16223  divalglem7  16312  divalg  16316  gcdaddm  16438  smadiadetr  22591  iblcnlem  25718  ax5seglem8  28916  elimnv  30665  elimnvu  30666  nmlno0i  30776  nmblolbi  30782  blocn  30789  elimphu  30803  ubth  30855  htth  30900  ifhvhv0  31004  normlem6  31097  norm-iii  31122  norm3lemt  31134  ifchhv  31226  hhssablo  31245  hhssnvt  31247  shscl  31300  shslej  31362  shincl  31363  omlsii  31385  pjoml  31418  pjoc2  31421  chm0  31473  chne0  31476  chocin  31477  chj0  31479  chlejb1  31494  chnle  31496  ledi  31522  h1datom  31564  cmbr3  31590  pjoml2  31593  cmcm  31596  cmcm3  31597  lecm  31599  pjmuli  31671  pjige0  31673  pjhfo  31688  pj11  31696  eigre  31817  eigorth  31820  hoddi  31972  nmlnop0  31980  lnopeq  31991  lnopunilem2  31993  nmbdoplb  32007  nmcopex  32011  nmcoplb  32012  lnopcon  32017  lnfn0  32029  lnfnmul  32030  nmcfnex  32035  nmcfnlb  32036  lnfncon  32038  riesz4  32046  riesz1  32047  cnlnadjeu  32060  pjhmop  32132  pjidmco  32163  mdslmd1lem3  32309  mdslmd1lem4  32310  csmdsymi  32316  hatomic  32342  atord  32370  atcvat2  32371  bnj941  34805  bnj944  34971  kur14  35281  abs2sqle  35745  abs2sqlt  35746  onsucconn  36503  onsucsuccmp  36509  sdclem1  37804  mnurnd  44401  bnd2d  49807