Theorem elex2 2776

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 2265	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1885	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2774	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1610	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  snmg  3736  oprcl  3828  brm  4079  ss1o0el1  4226  exss  4256  onintrab2im  4550  regexmidlemm  4564  dmxpid  4883  acexmidlem2  5915  frecabcl  6452  ixpm  6784  enm  6874  ssfilem  6931  fin0  6941  fin0or  6942  diffitest  6943  diffisn  6949  infm  6960  inffiexmid  6962  ctssdc  7172  omct  7176  ctssexmid  7209  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  caucvgsrlemasr  7850  suplocsrlempr  7867  gtso  8098  sup3exmid  8976  indstr  9658  negm  9680  fzm  10104  fzom  10231  rexfiuz  11133  r19.2uz  11137  resqrexlemgt0  11164  climuni  11436  bezoutlembi  12142  nninfct  12178  lcmgcdlem  12215  pcprecl  12427  pc2dvds  12468  4sqlem13m  12541  nninfdclemcl  12605  dfgrp3m  13171  issubg2m  13259  issubgrpd2  13260  issubg3  13262  issubg4m  13263  grpissubg  13264  subgintm  13268  nmzsubg  13280  ghmrn  13327  ghmpreima  13336  dvdsr02  13601  01eq0ring  13685  subrgugrp  13736  lmodfopnelem1  13820  rmodislmodlem  13846  rmodislmod  13847  lss1  13858  lsssubg  13873  islss3  13875  islss4  13878  lss1d  13879  lssintclm  13880  dflidl2rng  13977  lidlsubg  13982  cnsubglem  14067  tgioo  14714  elply2  14881  pw1nct  15493  nninfall  15499  nnnninfen  15511