Theorem elrabi 3644

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 2179, ax-11 2196, ax-12 2215. (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.

Step	Hyp	Ref	Expression
1		dfclel 2840	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2742	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 488	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2112	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2891	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2852	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 482	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 605	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1964	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3417	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2882	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811  [wsb 2100   ∈ wcel 2146  {cab 2741  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  ssrab2  4008  elfvmptrab1w  7032  elfvmptrab1  7033  elovmporab  7677  elovmporab1w  7678  elovmporab1  7679  elovmpt3rab1  7691  mapfienlem1  9410  mapfienlem2  9411  mapfienlem3  9412  scottelrankd  9961  kmlem1  10242  fin1a2lem9  10499  ac6num  10570  nnind  12366  ublbneg  13073  supminf  13075  rlimrege0  15761  incexc2  16022  lcmgcdlem  16796  phisum  16983  prmgaplem5  17248  isinitoi  18189  istermoi  18190  odcl  19765  odlem2  19768  gexcl  19809  gexlem2  19811  gexdvds  19813  pgpssslw  19843  psgnfix2  21920  psgndiflemB  21921  psgndif  21923  copsgndif  21924  psrbagf  22241  psrbagleadd1  22251  resspsrmul  22298  mplbas2  22366  rhmcomulmpl  22448  mhpmulcl  22485  psdmul  22502  mptcoe1fsupp  22548  psropprmul  22570  coe1mul2  22603  cpmatpmat  23043  mptcoe1matfsupp  23135  mp2pm2mplem4  23142  chpscmat  23175  chpscmatgsumbin  23177  chpscmatgsummon  23178  txdis1cn  23969  ptcmplem3  24388  rrxmvallem  25740  mdegmullem  26411  0sgm  27486  sgmf  27487  sgmnncl  27489  fsumdvdsdiaglem  27525  fsumdvdscom  27527  dvdsppwf1o  27528  dvdsflf1o  27529  musumsum  27534  muinv  27535  sgmppw  27539  rpvmasumlem  27829  dchrmusum2  27836  dchrvmasumlem1  27837  dchrvmasum2lem  27838  dchrisum0fmul  27848  dchrisum0ff  27849  dchrisum0flblem1  27850  dchrisum0  27862  logsqvma  27884  precsexlem9  28616  usgredg2v  29823  umgrres1lem  29906  upgrres1  29909  vtxdgoddnumeven  30149  rusgrnumwwlks  30581  frgrwopreglem4  30931  frgrwopreg  30939  rabsnel  33153  nnindf  33467  cyc3evpm  33767  cycpmgcl  33770  cycpmconjslem2  33772  elrgspnsubrun  33866  nsgmgclem  34018  mplvrpmrhm  34235  ddemeas  34925  imambfm  34950  eulerpartlemgs2  35068  ballotlemfc0  35181  ballotlemfcc  35182  ballotlemirc  35220  reprf  35297  tgoldbachgnn  35344  tgoldbachgt  35348  bnj110  35544  fnrelpredd  35784  wevgblacfn  35996  weiunlem  37381  poimirlem4  38685  poimirlem5  38686  poimirlem6  38687  poimirlem7  38688  poimirlem8  38689  poimirlem9  38690  poimirlem10  38691  poimirlem11  38692  poimirlem12  38693  poimirlem13  38694  poimirlem14  38695  poimirlem15  38696  poimirlem16  38697  poimirlem17  38698  poimirlem18  38699  poimirlem19  38700  poimirlem20  38701  poimirlem21  38702  poimirlem22  38703  poimirlem26  38707  mblfinlem2  38719  primrootsunit1  43290  hashscontpow1  43314  aks6d1c6lem2  43364  aks6d1c6lem3  43365  grpods  43387  rhmcomulpsr  43753  mhphflem  43767  mhphf  43768  rencldnfilem  43970  irrapx1  43978  radcnvrat  45441  supminfxr  46616  fsumiunss  46729  dvnprodlem1  47098  stoweidlem15  47167  stoweidlem31  47183  fourierdlem25  47284  fourierdlem51  47309  fourierdlem79  47337  etransclem28  47414  issalgend  47490  sge0iunmptlemre  47567  hoidmvlelem2  47748  issmflem  47879  smfresal  47940  2zrngasgrp  49485  2zrngamnd  49486  2zrngacmnd  49487  2zrngagrp  49488  2zrngmsgrp  49492  2zrngALT  49493  2zrngnmlid  49494  2zrngnmlid2  49496  dvsec  51073  dvcsc  51074  dvcot  51075