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

Theorem elrabi 3640
Description: Implication for the membership in a restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017.) Remove disjoint variable condition on 𝐴, 𝑥 and avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by SN, 5-Aug-2024.)
Assertion
Ref Expression
elrabi (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Distinct variable group:   𝑥,𝑉
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem elrabi
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfclel 2812 . . 3 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥 ∣ (𝑥𝑉𝜑)}))
2 df-clab 2711 . . . . . 6 (𝑦 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} ↔ [𝑦 / 𝑥](𝑥𝑉𝜑))
3 simpl 484 . . . . . . . 8 ((𝑥𝑉𝜑) → 𝑥𝑉)
43sbimi 2078 . . . . . . 7 ([𝑦 / 𝑥](𝑥𝑉𝜑) → [𝑦 / 𝑥]𝑥𝑉)
5 clelsb1 2861 . . . . . . 7 ([𝑦 / 𝑥]𝑥𝑉𝑦𝑉)
64, 5sylib 217 . . . . . 6 ([𝑦 / 𝑥](𝑥𝑉𝜑) → 𝑦𝑉)
72, 6sylbi 216 . . . . 5 (𝑦 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝑦𝑉)
8 eleq1 2822 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝑉𝐴𝑉))
98biimpa 478 . . . . 5 ((𝑦 = 𝐴𝑦𝑉) → 𝐴𝑉)
107, 9sylan2 594 . . . 4 ((𝑦 = 𝐴𝑦 ∈ {𝑥 ∣ (𝑥𝑉𝜑)}) → 𝐴𝑉)
1110exlimiv 1934 . . 3 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥 ∣ (𝑥𝑉𝜑)}) → 𝐴𝑉)
121, 11sylbi 216 . 2 (𝐴 ∈ {𝑥 ∣ (𝑥𝑉𝜑)} → 𝐴𝑉)
13 df-rab 3407 . 2 {𝑥𝑉𝜑} = {𝑥 ∣ (𝑥𝑉𝜑)}
1412, 13eleq2s 2852 1 (𝐴 ∈ {𝑥𝑉𝜑} → 𝐴𝑉)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wex 1782  [wsb 2068  wcel 2107  {cab 2710  {crab 3406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407
This theorem is referenced by:  ssrab2  4038  elfvmptrab1w  6975  elfvmptrab1  6976  elovmporab  7600  elovmporab1w  7601  elovmporab1  7602  elovmpt3rab1  7614  mapfienlem1  9346  mapfienlem2  9347  mapfienlem3  9348  kmlem1  10091  fin1a2lem9  10349  ac6num  10420  nnind  12176  ublbneg  12863  supminf  12865  rlimrege0  15467  incexc2  15728  lcmgcdlem  16487  phisum  16667  prmgaplem5  16932  isinitoi  17890  istermoi  17891  odcl  19323  odlem2  19326  gexcl  19367  gexlem2  19369  gexdvds  19371  pgpssslw  19401  psgnfix2  21019  psgndiflemB  21020  psgndif  21022  copsgndif  21023  psrbagf  21336  resspsrmul  21402  mplbas2  21459  mhpmulcl  21555  mptcoe1fsupp  21602  psropprmul  21625  coe1mul2  21656  cpmatpmat  22075  mptcoe1matfsupp  22167  mp2pm2mplem4  22174  chpscmat  22207  chpscmatgsumbin  22209  chpscmatgsummon  22210  txdis1cn  23002  ptcmplem3  23421  rrxmvallem  24784  mdegmullem  25459  0sgm  26509  sgmf  26510  sgmnncl  26512  fsumdvdsdiaglem  26548  fsumdvdscom  26550  dvdsppwf1o  26551  dvdsflf1o  26552  musumsum  26557  muinv  26558  sgmppw  26561  rpvmasumlem  26851  dchrmusum2  26858  dchrvmasumlem1  26859  dchrvmasum2lem  26860  dchrisum0fmul  26870  dchrisum0ff  26871  dchrisum0flblem1  26872  dchrisum0  26884  logsqvma  26906  usgredg2v  28217  umgrres1lem  28300  upgrres1  28303  vtxdgoddnumeven  28543  rusgrnumwwlks  28961  frgrwopreglem4  29301  frgrwopreg  29309  rabsnel  31471  nnindf  31764  cyc3evpm  32048  cycpmgcl  32051  cycpmconjslem2  32053  nsgmgclem  32237  ddemeas  32892  imambfm  32919  eulerpartlemgs2  33037  ballotlemfc0  33149  ballotlemfcc  33150  ballotlemirc  33188  reprf  33282  tgoldbachgnn  33329  tgoldbachgt  33333  bnj110  33527  fnrelpredd  33750  poimirlem4  36128  poimirlem5  36129  poimirlem6  36130  poimirlem7  36131  poimirlem8  36132  poimirlem9  36133  poimirlem10  36134  poimirlem11  36135  poimirlem12  36136  poimirlem13  36137  poimirlem14  36138  poimirlem15  36139  poimirlem16  36140  poimirlem17  36141  poimirlem18  36142  poimirlem19  36143  poimirlem20  36144  poimirlem21  36145  poimirlem22  36146  poimirlem26  36150  mblfinlem2  36162  mhphflem  40813  mhphf  40814  rencldnfilem  41186  irrapx1  41194  scottelrankd  42615  radcnvrat  42682  supminfxr  43785  fsumiunss  43902  dvnprodlem1  44273  stoweidlem15  44342  stoweidlem31  44358  fourierdlem25  44459  fourierdlem51  44484  fourierdlem79  44512  etransclem28  44589  issalgend  44665  sge0iunmptlemre  44742  hoidmvlelem2  44923  issmflem  45054  smfresal  45115  2zrngasgrp  46324  2zrngamnd  46325  2zrngacmnd  46326  2zrngagrp  46327  2zrngmsgrp  46331  2zrngALT  46332  2zrngnmlid  46333  2zrngnmlid2  46335
  Copyright terms: Public domain W3C validator