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

Theorem elrabi 3391
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 2777 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)))
2 eleq1 2718 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝑉𝐴𝑉))
32anbi1d 741 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝑉𝜑) ↔ (𝐴𝑉𝜑)))
43simprbda 652 . . . 4 ((𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
54exlimiv 1898 . . 3 (∃𝑥(𝑥 = 𝐴 ∧ (𝑥𝑉𝜑)) → 𝐴𝑉)
61, 5sylbi 207 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
7 df-rab 2950 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
86, 7eleq2s 2748 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wex 1744  wcel 2030  {cab 2637  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-rab 2950
This theorem is referenced by:  elfvmptrab1  6344  elovmpt2rab  6922  elovmpt2rab1  6923  elovmpt3rab1  6935  mapfienlem1  8351  mapfienlem2  8352  mapfienlem3  8353  kmlem1  9010  fin1a2lem9  9268  nnind  11076  ublbneg  11811  supminf  11813  rlimrege0  14354  incexc2  14614  lcmgcdlem  15366  phisum  15542  prmgaplem5  15806  isinitoi  16700  istermoi  16701  odcl  18001  odlem2  18004  gexcl  18041  gexlem2  18043  gexdvds  18045  pgpssslw  18075  resspsrmul  19465  mplbas2  19518  mptcoe1fsupp  19633  psropprmul  19656  coe1mul2  19687  psgnfix2  19993  psgndiflemB  19994  psgndif  19996  zrhcopsgndif  19997  cpmatpmat  20563  mptcoe1matfsupp  20655  mp2pm2mplem4  20662  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  txdis1cn  21486  ptcmplem3  21905  rrxmvallem  23233  mdegmullem  23883  0sgm  24915  sgmf  24916  sgmnncl  24918  fsumdvdsdiaglem  24954  fsumdvdscom  24956  dvdsppwf1o  24957  dvdsflf1o  24958  musumsum  24963  muinv  24964  sgmppw  24967  rpvmasumlem  25221  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrisum0fmul  25240  dchrisum0ff  25241  dchrisum0flblem1  25242  dchrisum0  25254  logsqvma  25276  usgredg2v  26164  umgrres1lem  26247  upgrres1  26250  vtxdgoddnumeven  26505  rusgrnumwwlks  26941  clwlksf1clwwlk  27056  frgrwopreglem4  27295  frgrwopreg  27303  rabsnel  29467  nnindf  29693  ddemeas  30427  imambfm  30452  eulerpartlemgs2  30570  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemirc  30721  reprf  30818  tgoldbachgnn  30865  tgoldbachgt  30869  bnj110  31054  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem26  33565  mblfinlem2  33577  rencldnfilem  37701  irrapx1  37709  radcnvrat  38830  supminfxr  40007  fsumiunss  40125  dvnprodlem1  40479  stoweidlem15  40550  stoweidlem31  40566  fourierdlem25  40667  fourierdlem51  40692  fourierdlem79  40720  etransclem28  40797  issalgend  40874  sge0iunmptlemre  40950  hoidmvlelem2  41131  issmflem  41257  smfresal  41316  2zrngasgrp  42265  2zrngamnd  42266  2zrngacmnd  42267  2zrngagrp  42268  2zrngmsgrp  42272  2zrngALT  42273  2zrngnmlid  42274  2zrngnmlid2  42276
  Copyright terms: Public domain W3C validator