Theorem elimel 4534

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

Syntax hints:   ∈ wcel 2110  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  fprg  6912  orduninsuc  7552  oawordeu  8175  oeoa  8217  omopth  8279  unfilem3  8778  inar1  10191  supsr  10528  renegcl  10943  peano5uzti  12066  eluzadd  12267  eluzsub  12268  ltweuz  13323  uzenom  13326  seqfn  13375  seq1  13376  seqp1  13378  sqeqor  13572  binom2  13573  nn0opth2  13626  faclbnd4lem2  13648  hashxp  13789  dvdsle  15654  divalglem7  15744  divalg  15748  gcdaddm  15867  smadiadetr  21278  iblcnlem  24383  ax5seglem8  26716  elimnv  28454  elimnvu  28455  nmlno0i  28565  nmblolbi  28571  blocn  28578  elimphu  28592  ubth  28644  htth  28689  ifhvhv0  28793  normlem6  28886  norm-iii  28911  norm3lemt  28923  ifchhv  29015  hhssablo  29034  hhssnvt  29036  shscl  29089  shslej  29151  shincl  29152  omlsii  29174  pjoml  29207  pjoc2  29210  chm0  29262  chne0  29265  chocin  29266  chj0  29268  chlejb1  29283  chnle  29285  ledi  29311  h1datom  29353  cmbr3  29379  pjoml2  29382  cmcm  29385  cmcm3  29386  lecm  29388  pjmuli  29460  pjige0  29462  pjhfo  29477  pj11  29485  eigre  29606  eigorth  29609  hoddi  29761  nmlnop0  29769  lnopeq  29780  lnopunilem2  29782  nmbdoplb  29796  nmcopex  29800  nmcoplb  29801  lnopcon  29806  lnfn0  29818  lnfnmul  29819  nmcfnex  29824  nmcfnlb  29825  lnfncon  29827  riesz4  29835  riesz1  29836  cnlnadjeu  29849  pjhmop  29921  pjidmco  29952  mdslmd1lem3  30098  mdslmd1lem4  30099  csmdsymi  30105  hatomic  30131  atord  30159  atcvat2  30160  bnj941  32039  bnj944  32205  kur14  32458  abs2sqle  32918  abs2sqlt  32919  onsucconn  33781  onsucsuccmp  33787  sdclem1  35012  mnurnd  40612  bnd2d  44777