MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrabi Structured version   Visualization version   GIF version

Theorem elrabi 3660
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.)
Assertion
Ref Expression
elrabi (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrabi
StepHypRef Expression
1 clelab 2959 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2903 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 632 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 502 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1932 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 220 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 3141 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2934 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wex 1781  wcel 2115  {cab 2802  {crab 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3141
This theorem is referenced by:  elfvmptrab1w  6775  elfvmptrab1  6776  elovmporab  7374  elovmporab1w  7375  elovmporab1  7376  elovmpt3rab1  7388  mapfienlem1  8852  mapfienlem2  8853  mapfienlem3  8854  kmlem1  9561  fin1a2lem9  9815  nnind  11641  ublbneg  12319  supminf  12321  rlimrege0  14925  incexc2  15182  lcmgcdlem  15937  phisum  16114  prmgaplem5  16378  isinitoi  17252  istermoi  17253  odcl  18653  odlem2  18656  gexcl  18694  gexlem2  18696  gexdvds  18698  pgpssslw  18728  resspsrmul  20183  mplbas2  20237  mptcoe1fsupp  20369  psropprmul  20392  coe1mul2  20423  psgnfix2  20729  psgndiflemB  20730  psgndif  20732  copsgndif  20733  cpmatpmat  21304  mptcoe1matfsupp  21396  mp2pm2mplem4  21403  chpscmat  21436  chpscmatgsumbin  21438  chpscmatgsummon  21439  txdis1cn  22229  ptcmplem3  22648  rrxmvallem  23997  mdegmullem  24668  0sgm  25718  sgmf  25719  sgmnncl  25721  fsumdvdsdiaglem  25757  fsumdvdscom  25759  dvdsppwf1o  25760  dvdsflf1o  25761  musumsum  25766  muinv  25767  sgmppw  25770  rpvmasumlem  26060  dchrmusum2  26067  dchrvmasumlem1  26068  dchrvmasum2lem  26069  dchrisum0fmul  26079  dchrisum0ff  26080  dchrisum0flblem1  26081  dchrisum0  26093  logsqvma  26115  usgredg2v  27006  umgrres1lem  27089  upgrres1  27092  vtxdgoddnumeven  27332  rusgrnumwwlks  27749  frgrwopreglem4  28089  frgrwopreg  28097  rabsnel  30258  nnindf  30532  cyc3evpm  30810  cycpmgcl  30813  cycpmconjslem2  30815  ddemeas  31513  imambfm  31538  eulerpartlemgs2  31656  ballotlemfc0  31768  ballotlemfcc  31769  ballotlemirc  31807  reprf  31901  tgoldbachgnn  31948  tgoldbachgt  31952  bnj110  32148  poimirlem4  34961  poimirlem5  34962  poimirlem6  34963  poimirlem7  34964  poimirlem8  34965  poimirlem9  34966  poimirlem10  34967  poimirlem11  34968  poimirlem12  34969  poimirlem13  34970  poimirlem14  34971  poimirlem15  34972  poimirlem16  34973  poimirlem17  34974  poimirlem18  34975  poimirlem19  34976  poimirlem20  34977  poimirlem21  34978  poimirlem22  34979  poimirlem26  34983  mblfinlem2  34995  rencldnfilem  39593  irrapx1  39601  scottelrankd  40791  radcnvrat  40854  supminfxr  41945  fsumiunss  42059  dvnprodlem1  42430  stoweidlem15  42499  stoweidlem31  42515  fourierdlem25  42616  fourierdlem51  42641  fourierdlem79  42669  etransclem28  42746  issalgend  42820  sge0iunmptlemre  42896  hoidmvlelem2  43077  issmflem  43203  smfresal  43262  2zrngasgrp  44406  2zrngamnd  44407  2zrngacmnd  44408  2zrngagrp  44409  2zrngmsgrp  44413  2zrngALT  44414  2zrngnmlid  44415  2zrngnmlid2  44417
  Copyright terms: Public domain W3C validator