Theorem elex2 2779

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)

Assertion

Ref	Expression
elex2	⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elex2

Step	Hyp	Ref	Expression
1		eleq1a 2268	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1888	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2777	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1613	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  snmg  3740  oprcl  3832  brm  4083  ss1o0el1  4230  exss  4260  onintrab2im  4554  regexmidlemm  4568  dmxpid  4887  acexmidlem2  5919  frecabcl  6457  ixpm  6789  enm  6879  ssfilem  6936  fin0  6946  fin0or  6947  diffitest  6948  diffisn  6954  infm  6965  inffiexmid  6967  ctssdc  7179  omct  7183  ctssexmid  7216  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  caucvgsrlemasr  7857  suplocsrlempr  7874  gtso  8105  sup3exmid  8984  indstr  9667  negm  9689  fzm  10113  fzom  10240  rexfiuz  11154  r19.2uz  11158  resqrexlemgt0  11185  climuni  11458  bezoutlembi  12172  nninfct  12208  lcmgcdlem  12245  pcprecl  12458  pc2dvds  12499  4sqlem13m  12572  nninfdclemcl  12665  dfgrp3m  13231  issubg2m  13319  issubgrpd2  13320  issubg3  13322  issubg4m  13323  grpissubg  13324  subgintm  13328  nmzsubg  13340  ghmrn  13387  ghmpreima  13396  dvdsr02  13661  01eq0ring  13745  subrgugrp  13796  lmodfopnelem1  13880  rmodislmodlem  13906  rmodislmod  13907  lss1  13918  lsssubg  13933  islss3  13935  islss4  13938  lss1d  13939  lssintclm  13940  dflidl2rng  14037  lidlsubg  14042  cnsubglem  14135  tgioo  14790  elply2  14971  pw1nct  15647  nninfall  15653  nnnninfen  15665