Theorem elimel 4558

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

Syntax hints:   ∈ wcel 2109  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  fprg  7127  orduninsuc  7819  oawordeu  8519  oeoa  8561  omopth  8626  unfilem3  9256  inar1  10728  supsr  11065  renegcl  11485  peano5uzti  12624  eluzaddOLD  12828  eluzsubOLD  12829  ltweuz  13926  uzenom  13929  seqfn  13978  seq1  13979  seqp1  13981  sqeqor  14181  binom2  14182  nn0opth2  14237  faclbnd4lem2  14259  hashxp  14399  dvdsle  16280  divalglem7  16369  divalg  16373  gcdaddm  16495  smadiadetr  22562  iblcnlem  25690  ax5seglem8  28863  elimnv  30612  elimnvu  30613  nmlno0i  30723  nmblolbi  30729  blocn  30736  elimphu  30750  ubth  30802  htth  30847  ifhvhv0  30951  normlem6  31044  norm-iii  31069  norm3lemt  31081  ifchhv  31173  hhssablo  31192  hhssnvt  31194  shscl  31247  shslej  31309  shincl  31310  omlsii  31332  pjoml  31365  pjoc2  31368  chm0  31420  chne0  31423  chocin  31424  chj0  31426  chlejb1  31441  chnle  31443  ledi  31469  h1datom  31511  cmbr3  31537  pjoml2  31540  cmcm  31543  cmcm3  31544  lecm  31546  pjmuli  31618  pjige0  31620  pjhfo  31635  pj11  31643  eigre  31764  eigorth  31767  hoddi  31919  nmlnop0  31927  lnopeq  31938  lnopunilem2  31940  nmbdoplb  31954  nmcopex  31958  nmcoplb  31959  lnopcon  31964  lnfn0  31976  lnfnmul  31977  nmcfnex  31982  nmcfnlb  31983  lnfncon  31985  riesz4  31993  riesz1  31994  cnlnadjeu  32007  pjhmop  32079  pjidmco  32110  mdslmd1lem3  32256  mdslmd1lem4  32257  csmdsymi  32263  hatomic  32289  atord  32317  atcvat2  32318  bnj941  34762  bnj944  34928  kur14  35203  abs2sqle  35667  abs2sqlt  35668  onsucconn  36426  onsucsuccmp  36432  sdclem1  37737  mnurnd  44272  bnd2d  49670