Theorem sseli 3224

Description: Membership inference from subclass relationship. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
sseli.1	⊢ 𝐴 ⊆ 𝐵

Assertion

Ref	Expression
sseli	⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		ssel 3222	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sselii  3225  sselid  3226  elun1  3376  elun2  3377  elopabr  4383  elopabran  4384  finds  4704  finds2  4705  issref  5126  2elresin  5450  fvun1  5721  fvmptssdm  5740  elfvmptrab1  5750  fvimacnvi  5770  elpreima  5775  ofrfval  6253  ofvalg  6254  off  6257  offres  6306  eqopi  6344  op1steq  6351  dfoprab4  6364  f1od2  6409  reldmtpos  6462  smores3  6502  smores2  6503  ctssdccl  7353  pinn  7572  indpi  7605  enq0enq  7694  preqlu  7735  elinp  7737  prop  7738  elnp1st2nd  7739  prarloclem5  7763  cauappcvgprlemladd  7921  peano5nnnn  8155  nnindnn  8156  recn  8208  rexr  8267  peano5nni  9188  nnre  9192  nncn  9193  nnind  9201  nnnn0  9451  nn0re  9453  nn0cn  9454  nn0xnn0  9513  nnz  9542  nn0z  9543  uzuzle35  9843  nnq  9911  qcn  9912  rpre  9939  iccshftri  10274  iccshftli  10276  iccdili  10278  icccntri  10280  fzval2  10291  fzelp1  10354  4fvwrd4  10420  elfzo1  10476  infssuzcldc  10541  expcllem  10858  expcl2lemap  10859  m1expcl2  10869  bcm1k  11068  bcpasc  11074  wrdv  11178  ccatclab  11220  pfxfv0  11322  pfxfvlsw  11325  cau3lem  11737  climconst2  11914  fsum3  12011  binomlem  12107  fprodge1  12263  cos12dec  12392  dvdsflip  12475  isprm3  12753  phimullem  12860  prmdiveq  12871  structcnvcnv  13161  fvsetsid  13179  ptex  13410  nmzsubg  13860  nmznsg  13863  nzrring  14261  lringnzr  14271  rege0subm  14663  znrrg  14739  psrbagconf1o  14757  tgval2  14845  qtopbasss  15315  dedekindicc  15427  ivthinc  15437  ivthdec  15438  dvply2  15561  cosz12  15574  cos0pilt1  15646  ioocosf1o  15648  mpodvdsmulf1o  15787  fsumdvdsmul  15788  lgsquadlemofi  15878  lgsquadlem1  15879  lgsquadlem2  15880  wlk1walkdom  16283  exmidsbthrlem  16733