Theorem elex2 2787

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 2276	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1896	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2785	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1621	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1370   = wceq 1372  ∃wex 1514   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  snmg  3750  oprcl  3842  brm  4093  ss1o0el1  4240  exss  4270  onintrab2im  4564  regexmidlemm  4578  dmxpid  4897  acexmidlem2  5931  frecabcl  6475  ixpm  6807  enm  6897  ssfilem  6954  fin0  6964  fin0or  6965  diffitest  6966  diffisn  6972  infm  6983  inffiexmid  6985  ctssdc  7197  omct  7201  ctssexmid  7234  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  acnrcl  7295  exmidaclem  7302  caucvgsrlemasr  7885  suplocsrlempr  7902  gtso  8133  sup3exmid  9012  indstr  9696  negm  9718  fzm  10142  fzom  10269  rexfiuz  11219  r19.2uz  11223  resqrexlemgt0  11250  climuni  11523  bezoutlembi  12245  nninfct  12281  lcmgcdlem  12318  pcprecl  12531  pc2dvds  12572  4sqlem13m  12645  nninfdclemcl  12738  dfgrp3m  13349  issubg2m  13443  issubgrpd2  13444  issubg3  13446  issubg4m  13447  grpissubg  13448  subgintm  13452  nmzsubg  13464  ghmrn  13511  ghmpreima  13520  dvdsr02  13785  01eq0ring  13869  subrgugrp  13920  lmodfopnelem1  14004  rmodislmodlem  14030  rmodislmod  14031  lss1  14042  lsssubg  14057  islss3  14059  islss4  14062  lss1d  14063  lssintclm  14064  dflidl2rng  14161  lidlsubg  14166  cnsubglem  14259  tgioo  14944  elply2  15125  pw1nct  15804  nninfall  15810  nnnninfen  15822