Theorem elimel 4483

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

Syntax hints:   ∈ wcel 2114  ifcif 4414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-if 4415

This theorem is referenced by:  fprg  6927  orduninsuc  7577  oawordeu  8212  oeoa  8254  omopth  8316  unfilem3  8858  inar1  10275  supsr  10612  renegcl  11027  peano5uzti  12153  eluzadd  12355  eluzsub  12356  ltweuz  13420  uzenom  13423  seqfn  13472  seq1  13473  seqp1  13475  sqeqor  13670  binom2  13671  nn0opth2  13724  faclbnd4lem2  13746  hashxp  13887  dvdsle  15755  divalglem7  15844  divalg  15848  gcdaddm  15968  smadiadetr  21426  iblcnlem  24541  ax5seglem8  26882  elimnv  28618  elimnvu  28619  nmlno0i  28729  nmblolbi  28735  blocn  28742  elimphu  28756  ubth  28808  htth  28853  ifhvhv0  28957  normlem6  29050  norm-iii  29075  norm3lemt  29087  ifchhv  29179  hhssablo  29198  hhssnvt  29200  shscl  29253  shslej  29315  shincl  29316  omlsii  29338  pjoml  29371  pjoc2  29374  chm0  29426  chne0  29429  chocin  29430  chj0  29432  chlejb1  29447  chnle  29449  ledi  29475  h1datom  29517  cmbr3  29543  pjoml2  29546  cmcm  29549  cmcm3  29550  lecm  29552  pjmuli  29624  pjige0  29626  pjhfo  29641  pj11  29649  eigre  29770  eigorth  29773  hoddi  29925  nmlnop0  29933  lnopeq  29944  lnopunilem2  29946  nmbdoplb  29960  nmcopex  29964  nmcoplb  29965  lnopcon  29970  lnfn0  29982  lnfnmul  29983  nmcfnex  29988  nmcfnlb  29989  lnfncon  29991  riesz4  29999  riesz1  30000  cnlnadjeu  30013  pjhmop  30085  pjidmco  30116  mdslmd1lem3  30262  mdslmd1lem4  30263  csmdsymi  30269  hatomic  30295  atord  30323  atcvat2  30324  bnj941  32323  bnj944  32489  kur14  32749  abs2sqle  33209  abs2sqlt  33210  onsucconn  34265  onsucsuccmp  34271  sdclem1  35524  mnurnd  41443  bnd2d  45840