Theorem sselid 3153

Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)

Hypotheses

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵
sselid.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sselid	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sselid

Step	Hyp	Ref	Expression
1		sselid.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseli.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
3	2	sseli 3151	. 2 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2148   ⊆ wss 3129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  mptrcl  5598  riotacl  5844  riotasbc  5845  elmpocl  6068  ofrval  6092  f1od2  6235  mpoxopn0yelv  6239  tpostpos  6264  smores  6292  supubti  6997  suplubti  6998  nninfwlporlemd  7169  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  prarloclemcalc  7500  rereceu  7887  recriota  7888  rexrd  8006  eqord1  8439  nnred  8931  nncnd  8932  un0addcl  9208  un0mulcl  9209  nnnn0d  9228  nn0red  9229  nn0xnn0d  9247  suprzclex  9350  nn0zd  9372  zred  9374  rpred  9695  ige2m1fz  10109  zmodfzp1  10347  seq3caopr2  10481  expcl2lemap  10531  m1expcl  10542  summodclem2a  11388  zsumdc  11391  clim2prod  11546  ntrivcvgap  11555  prodmodclem2a  11583  zproddc  11586  zsupssdc  11954  lcmn0cl  12067  isprm5lem  12140  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  prmdivdiv  12236  ennnfonelemg  12403  nmzsubg  13068  lmrcl  13661  lmss  13716  upxp  13742  isxms2  13922  iooretopg  13998  tgqioo  14017  limccoap  14117  dvcl  14122  dvidlemap  14130  dvcnp2cntop  14133  lgscl  14385  2sqlem6  14437  2sqlem8  14440  2sqlem9  14441  isomninnlem  14748  trilpolemeq1  14758  trilpolemlt1  14759  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770  nconstwlpolemgt0  14781