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  4565  regexmidlemm  4579  dmxpid  4898  acexmidlem2  5940  frecabcl  6484  ixpm  6816  enm  6914  ssfilem  6971  fin0  6981  fin0or  6982  diffitest  6983  diffisn  6989  infm  7000  inffiexmid  7002  ctssdc  7214  omct  7218  ctssexmid  7251  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  acnrcl  7312  exmidaclem  7319  caucvgsrlemasr  7902  suplocsrlempr  7919  gtso  8150  sup3exmid  9029  indstr  9713  negm  9735  fzm  10159  fzom  10286  rexfiuz  11242  r19.2uz  11246  resqrexlemgt0  11273  climuni  11546  bezoutlembi  12268  nninfct  12304  lcmgcdlem  12341  pcprecl  12554  pc2dvds  12595  4sqlem13m  12668  nninfdclemcl  12761  dfgrp3m  13373  issubg2m  13467  issubgrpd2  13468  issubg3  13470  issubg4m  13471  grpissubg  13472  subgintm  13476  nmzsubg  13488  ghmrn  13535  ghmpreima  13544  dvdsr02  13809  01eq0ring  13893  subrgugrp  13944  lmodfopnelem1  14028  rmodislmodlem  14054  rmodislmod  14055  lss1  14066  lsssubg  14081  islss3  14083  islss4  14086  lss1d  14087  lssintclm  14088  dflidl2rng  14185  lidlsubg  14190  cnsubglem  14283  tgioo  14968  elply2  15149  pw1nct  15873  nninfall  15879  nnnninfen  15891