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  3741  oprcl  3833  brm  4084  ss1o0el1  4231  exss  4261  onintrab2im  4555  regexmidlemm  4569  dmxpid  4888  acexmidlem2  5922  frecabcl  6466  ixpm  6798  enm  6888  ssfilem  6945  fin0  6955  fin0or  6956  diffitest  6957  diffisn  6963  infm  6974  inffiexmid  6976  ctssdc  7188  omct  7192  ctssexmid  7225  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  acnrcl  7286  exmidaclem  7293  caucvgsrlemasr  7876  suplocsrlempr  7893  gtso  8124  sup3exmid  9003  indstr  9686  negm  9708  fzm  10132  fzom  10259  rexfiuz  11173  r19.2uz  11177  resqrexlemgt0  11204  climuni  11477  bezoutlembi  12199  nninfct  12235  lcmgcdlem  12272  pcprecl  12485  pc2dvds  12526  4sqlem13m  12599  nninfdclemcl  12692  dfgrp3m  13303  issubg2m  13397  issubgrpd2  13398  issubg3  13400  issubg4m  13401  grpissubg  13402  subgintm  13406  nmzsubg  13418  ghmrn  13465  ghmpreima  13474  dvdsr02  13739  01eq0ring  13823  subrgugrp  13874  lmodfopnelem1  13958  rmodislmodlem  13984  rmodislmod  13985  lss1  13996  lsssubg  14011  islss3  14013  islss4  14016  lss1d  14017  lssintclm  14018  dflidl2rng  14115  lidlsubg  14120  cnsubglem  14213  tgioo  14898  elply2  15079  pw1nct  15758  nninfall  15764  nnnninfen  15776