Theorem elimel 4617

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

Syntax hints:   ∈ wcel 2108  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  fprg  7189  orduninsuc  7880  oawordeu  8611  oeoa  8653  omopth  8718  unfilem3  9373  inar1  10844  supsr  11181  renegcl  11599  peano5uzti  12733  eluzaddOLD  12938  eluzsubOLD  12939  ltweuz  14012  uzenom  14015  seqfn  14064  seq1  14065  seqp1  14067  sqeqor  14265  binom2  14266  nn0opth2  14321  faclbnd4lem2  14343  hashxp  14483  dvdsle  16358  divalglem7  16447  divalg  16451  gcdaddm  16571  smadiadetr  22702  iblcnlem  25844  ax5seglem8  28969  elimnv  30715  elimnvu  30716  nmlno0i  30826  nmblolbi  30832  blocn  30839  elimphu  30853  ubth  30905  htth  30950  ifhvhv0  31054  normlem6  31147  norm-iii  31172  norm3lemt  31184  ifchhv  31276  hhssablo  31295  hhssnvt  31297  shscl  31350  shslej  31412  shincl  31413  omlsii  31435  pjoml  31468  pjoc2  31471  chm0  31523  chne0  31526  chocin  31527  chj0  31529  chlejb1  31544  chnle  31546  ledi  31572  h1datom  31614  cmbr3  31640  pjoml2  31643  cmcm  31646  cmcm3  31647  lecm  31649  pjmuli  31721  pjige0  31723  pjhfo  31738  pj11  31746  eigre  31867  eigorth  31870  hoddi  32022  nmlnop0  32030  lnopeq  32041  lnopunilem2  32043  nmbdoplb  32057  nmcopex  32061  nmcoplb  32062  lnopcon  32067  lnfn0  32079  lnfnmul  32080  nmcfnex  32085  nmcfnlb  32086  lnfncon  32088  riesz4  32096  riesz1  32097  cnlnadjeu  32110  pjhmop  32182  pjidmco  32213  mdslmd1lem3  32359  mdslmd1lem4  32360  csmdsymi  32366  hatomic  32392  atord  32420  atcvat2  32421  bnj941  34748  bnj944  34914  kur14  35184  abs2sqle  35648  abs2sqlt  35649  onsucconn  36404  onsucsuccmp  36410  sdclem1  37703  mnurnd  44252  bnd2d  48773