Theorem elimel 4537

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

Syntax hints:   ∈ wcel 2114  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  fprg  7102  orduninsuc  7787  oawordeu  8483  oeoa  8526  omopth  8591  unfilem3  9210  inar1  10689  supsr  11026  renegcl  11448  peano5uzti  12610  ltweuz  13914  uzenom  13917  seqfn  13966  seq1  13967  seqp1  13969  sqeqor  14169  binom2  14170  nn0opth2  14225  faclbnd4lem2  14247  hashxp  14387  dvdsle  16270  divalglem7  16359  divalg  16363  gcdaddm  16485  smadiadetr  22650  iblcnlem  25766  ax5seglem8  29019  elimnv  30769  elimnvu  30770  nmlno0i  30880  nmblolbi  30886  blocn  30893  elimphu  30907  ubth  30959  htth  31004  ifhvhv0  31108  normlem6  31201  norm-iii  31226  norm3lemt  31238  ifchhv  31330  hhssablo  31349  hhssnvt  31351  shscl  31404  shslej  31466  shincl  31467  omlsii  31489  pjoml  31522  pjoc2  31525  chm0  31577  chne0  31580  chocin  31581  chj0  31583  chlejb1  31598  chnle  31600  ledi  31626  h1datom  31668  cmbr3  31694  pjoml2  31697  cmcm  31700  cmcm3  31701  lecm  31703  pjmuli  31775  pjige0  31777  pjhfo  31792  pj11  31800  eigre  31921  eigorth  31924  hoddi  32076  nmlnop0  32084  lnopeq  32095  lnopunilem2  32097  nmbdoplb  32111  nmcopex  32115  nmcoplb  32116  lnopcon  32121  lnfn0  32133  lnfnmul  32134  nmcfnex  32139  nmcfnlb  32140  lnfncon  32142  riesz4  32150  riesz1  32151  cnlnadjeu  32164  pjhmop  32236  pjidmco  32267  mdslmd1lem3  32413  mdslmd1lem4  32414  csmdsymi  32420  hatomic  32446  atord  32474  atcvat2  32475  bnj941  34931  bnj944  35096  kur14  35414  abs2sqle  35878  abs2sqlt  35879  onsucconn  36636  onsucsuccmp  36642  sdclem1  38078  mnurnd  44728  bnd2d  50168