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

Theorem elrabi 3347
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 2751 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2692 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 740 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 652 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1860 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 207 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2921 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2722 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wex 1701  wcel 1992  {cab 2612  {crab 2916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-rab 2921
This theorem is referenced by:  elfvmptrab1  6262  elovmpt2rab  6834  elovmpt2rab1  6835  elovmpt3rab1  6847  mapfienlem1  8255  mapfienlem2  8256  mapfienlem3  8257  kmlem1  8917  fin1a2lem9  9175  nnind  10983  ublbneg  11717  supminf  11719  rlimrege0  14239  incexc2  14490  lcmgcdlem  15238  phisum  15414  prmgaplem5  15678  isinitoi  16569  istermoi  16570  odcl  17871  odlem2  17874  gexcl  17911  gexlem2  17913  gexdvds  17915  pgpssslw  17945  resspsrmul  19331  mplbas2  19384  mptcoe1fsupp  19499  psropprmul  19522  coe1mul2  19553  psgnfix2  19859  psgndiflemB  19860  psgndif  19862  zrhcopsgndif  19863  cpmatpmat  20429  mptcoe1matfsupp  20521  mp2pm2mplem4  20528  chpscmat  20561  chpscmatgsumbin  20563  chpscmatgsummon  20564  txdis1cn  21343  ptcmplem3  21763  rrxmvallem  23090  mdegmullem  23737  0sgm  24765  sgmf  24766  sgmnncl  24768  fsumdvdsdiaglem  24804  fsumdvdscom  24806  dvdsppwf1o  24807  dvdsflf1o  24808  musumsum  24813  muinv  24814  sgmppw  24817  rpvmasumlem  25071  dchrmusum2  25078  dchrvmasumlem1  25079  dchrvmasum2lem  25080  dchrisum0fmul  25090  dchrisum0ff  25091  dchrisum0flblem1  25092  dchrisum0  25104  logsqvma  25126  usgredg2v  26006  umgrres1lem  26084  upgrres1  26087  uvtxaisvtx  26170  rusgrnumwwlks  26730  clwlksf1clwwlk  26829  frgrwopreglem4  27036  frgrwopreg  27038  rabsnel  29180  nnindf  29398  ddemeas  30072  imambfm  30097  eulerpartlemgs2  30215  ballotlemfc0  30327  ballotlemfcc  30328  ballotlemirc  30366  bnj110  30628  poimirlem4  33031  poimirlem5  33032  poimirlem6  33033  poimirlem7  33034  poimirlem8  33035  poimirlem9  33036  poimirlem10  33037  poimirlem11  33038  poimirlem12  33039  poimirlem13  33040  poimirlem14  33041  poimirlem15  33042  poimirlem16  33043  poimirlem17  33044  poimirlem18  33045  poimirlem19  33046  poimirlem20  33047  poimirlem21  33048  poimirlem22  33049  poimirlem26  33053  mblfinlem2  33065  rencldnfilem  36850  irrapx1  36858  radcnvrat  37981  fsumiunss  39198  dvnprodlem1  39454  stoweidlem15  39526  stoweidlem31  39542  fourierdlem25  39643  fourierdlem51  39668  fourierdlem79  39696  etransclem28  39773  issalgend  39850  sge0iunmptlemre  39926  hoidmvlelem2  40104  issmflem  40230  smfresal  40289  2zrngasgrp  41201  2zrngamnd  41202  2zrngacmnd  41203  2zrngagrp  41204  2zrngmsgrp  41208  2zrngALT  41209  2zrngnmlid  41210  2zrngnmlid2  41212
  Copyright terms: Public domain W3C validator