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 2147, ax-11 2163, ax-12 2185. (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 2813	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2716	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2080	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2864	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2825	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 594	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1932	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3402	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2855	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781  [wsb 2068   ∈ wcel 2114  {cab 2715  {crab 3401

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  ssrab2  4034  elfvmptrab1w  6979  elfvmptrab1  6980  elovmporab  7616  elovmporab1w  7617  elovmporab1  7618  elovmpt3rab1  7630  mapfienlem1  9322  mapfienlem2  9323  mapfienlem3  9324  kmlem1  10075  fin1a2lem9  10332  ac6num  10403  nnind  12177  ublbneg  12860  supminf  12862  rlimrege0  15516  incexc2  15775  lcmgcdlem  16547  phisum  16732  prmgaplem5  16997  isinitoi  17937  istermoi  17938  odcl  19482  odlem2  19485  gexcl  19526  gexlem2  19528  gexdvds  19530  pgpssslw  19560  psgnfix2  21571  psgndiflemB  21572  psgndif  21574  copsgndif  21575  psrbagf  21891  psrbagleadd1  21901  resspsrmul  21948  mplbas2  22014  mhpmulcl  22109  psdmul  22126  mptcoe1fsupp  22173  psropprmul  22195  coe1mul2  22228  rhmcomulmpl  22343  cpmatpmat  22671  mptcoe1matfsupp  22763  mp2pm2mplem4  22770  chpscmat  22803  chpscmatgsumbin  22805  chpscmatgsummon  22806  txdis1cn  23596  ptcmplem3  24015  rrxmvallem  25377  mdegmullem  26056  0sgm  27127  sgmf  27128  sgmnncl  27130  fsumdvdsdiaglem  27166  fsumdvdscom  27168  dvdsppwf1o  27169  dvdsflf1o  27170  musumsum  27175  muinv  27176  sgmppw  27181  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumlem1  27479  dchrvmasum2lem  27480  dchrisum0fmul  27490  dchrisum0ff  27491  dchrisum0flblem1  27492  dchrisum0  27504  logsqvma  27526  precsexlem9  28228  usgredg2v  29318  umgrres1lem  29401  upgrres1  29404  vtxdgoddnumeven  29645  rusgrnumwwlks  30068  frgrwopreglem4  30408  frgrwopreg  30416  rabsnel  32593  nnindf  32917  cyc3evpm  33250  cycpmgcl  33253  cycpmconjslem2  33255  elrgspnsubrun  33349  nsgmgclem  33510  mplvrpmrhm  33730  ddemeas  34420  imambfm  34446  eulerpartlemgs2  34564  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemirc  34716  reprf  34796  tgoldbachgnn  34843  tgoldbachgt  34847  bnj110  35040  fnrelpredd  35274  wevgblacfn  35331  weiunlem  36685  poimirlem4  37904  poimirlem5  37905  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem9  37909  poimirlem10  37910  poimirlem11  37911  poimirlem12  37912  poimirlem13  37913  poimirlem14  37914  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem18  37918  poimirlem19  37919  poimirlem20  37920  poimirlem21  37921  poimirlem22  37922  poimirlem26  37926  mblfinlem2  37938  primrootsunit1  42496  hashscontpow1  42520  aks6d1c6lem2  42570  aks6d1c6lem3  42571  grpods  42593  rhmcomulpsr  42948  mhphflem  42983  mhphf  42984  rencldnfilem  43206  irrapx1  43214  scottelrankd  44632  radcnvrat  44699  supminfxr  45851  fsumiunss  45964  dvnprodlem1  46333  stoweidlem15  46402  stoweidlem31  46418  fourierdlem25  46519  fourierdlem51  46544  fourierdlem79  46572  etransclem28  46649  issalgend  46725  sge0iunmptlemre  46802  hoidmvlelem2  46983  issmflem  47114  smfresal  47175  2zrngasgrp  48635  2zrngamnd  48636  2zrngacmnd  48637  2zrngagrp  48638  2zrngmsgrp  48642  2zrngALT  48643  2zrngnmlid  48644  2zrngnmlid2  48646