Theorem elimel 4601

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

Syntax hints:   ∈ wcel 2098  ifcif 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4533

This theorem is referenced by:  fprg  7170  orduninsuc  7853  oawordeu  8582  oeoa  8624  omopth  8689  unfilem3  9343  inar1  10806  supsr  11143  renegcl  11561  peano5uzti  12690  eluzaddOLD  12895  eluzsubOLD  12896  ltweuz  13966  uzenom  13969  seqfn  14018  seq1  14019  seqp1  14021  sqeqor  14219  binom2  14220  nn0opth2  14271  faclbnd4lem2  14293  hashxp  14433  dvdsle  16294  divalglem7  16383  divalg  16387  gcdaddm  16507  smadiadetr  22597  iblcnlem  25738  ax5seglem8  28767  elimnv  30513  elimnvu  30514  nmlno0i  30624  nmblolbi  30630  blocn  30637  elimphu  30651  ubth  30703  htth  30748  ifhvhv0  30852  normlem6  30945  norm-iii  30970  norm3lemt  30982  ifchhv  31074  hhssablo  31093  hhssnvt  31095  shscl  31148  shslej  31210  shincl  31211  omlsii  31233  pjoml  31266  pjoc2  31269  chm0  31321  chne0  31324  chocin  31325  chj0  31327  chlejb1  31342  chnle  31344  ledi  31370  h1datom  31412  cmbr3  31438  pjoml2  31441  cmcm  31444  cmcm3  31445  lecm  31447  pjmuli  31519  pjige0  31521  pjhfo  31536  pj11  31544  eigre  31665  eigorth  31668  hoddi  31820  nmlnop0  31828  lnopeq  31839  lnopunilem2  31841  nmbdoplb  31855  nmcopex  31859  nmcoplb  31860  lnopcon  31865  lnfn0  31877  lnfnmul  31878  nmcfnex  31883  nmcfnlb  31884  lnfncon  31886  riesz4  31894  riesz1  31895  cnlnadjeu  31908  pjhmop  31980  pjidmco  32011  mdslmd1lem3  32157  mdslmd1lem4  32158  csmdsymi  32164  hatomic  32190  atord  32218  atcvat2  32219  bnj941  34436  bnj944  34602  kur14  34859  abs2sqle  35317  abs2sqlt  35318  onsucconn  35955  onsucsuccmp  35961  sdclem1  37249  mnurnd  43751  bnd2d  48190

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »