Theorem elrabi 3582

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 2145, ax-11 2162, ax-12 2179. (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 2812	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2717	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 486	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2084	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb3 2860	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2820	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 480	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 596	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1937	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3062	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2851	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542  ∃wex 1786  [wsb 2074   ∈ wcel 2114  {cab 2716  {crab 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062

This theorem is referenced by:  ssrab2  3969  elfvmptrab1w  6801  elfvmptrab1  6802  elovmporab  7407  elovmporab1w  7408  elovmporab1  7409  elovmpt3rab1  7421  mapfienlem1  8942  mapfienlem2  8943  mapfienlem3  8944  kmlem1  9650  fin1a2lem9  9908  ac6num  9979  nnind  11734  ublbneg  12415  supminf  12417  rlimrege0  15026  incexc2  15286  lcmgcdlem  16047  phisum  16227  prmgaplem5  16491  isinitoi  17371  istermoi  17372  odcl  18782  odlem2  18785  gexcl  18823  gexlem2  18825  gexdvds  18827  pgpssslw  18857  psgnfix2  20415  psgndiflemB  20416  psgndif  20418  copsgndif  20419  psrbagf  20731  resspsrmul  20796  mplbas2  20853  mhpmulcl  20943  mptcoe1fsupp  20990  psropprmul  21013  coe1mul2  21044  cpmatpmat  21461  mptcoe1matfsupp  21553  mp2pm2mplem4  21560  chpscmat  21593  chpscmatgsumbin  21595  chpscmatgsummon  21596  txdis1cn  22386  ptcmplem3  22805  rrxmvallem  24156  mdegmullem  24831  0sgm  25881  sgmf  25882  sgmnncl  25884  fsumdvdsdiaglem  25920  fsumdvdscom  25922  dvdsppwf1o  25923  dvdsflf1o  25924  musumsum  25929  muinv  25930  sgmppw  25933  rpvmasumlem  26223  dchrmusum2  26230  dchrvmasumlem1  26231  dchrvmasum2lem  26232  dchrisum0fmul  26242  dchrisum0ff  26243  dchrisum0flblem1  26244  dchrisum0  26256  logsqvma  26278  usgredg2v  27169  umgrres1lem  27252  upgrres1  27255  vtxdgoddnumeven  27495  rusgrnumwwlks  27912  frgrwopreglem4  28252  frgrwopreg  28260  rabsnel  30421  nnindf  30708  cyc3evpm  30994  cycpmgcl  30997  cycpmconjslem2  30999  nsgmgclem  31168  ddemeas  31774  imambfm  31799  eulerpartlemgs2  31917  ballotlemfc0  32029  ballotlemfcc  32030  ballotlemirc  32068  reprf  32162  tgoldbachgnn  32209  tgoldbachgt  32213  bnj110  32409  fnrelpredd  32632  poimirlem4  35404  poimirlem5  35405  poimirlem6  35406  poimirlem7  35407  poimirlem8  35408  poimirlem9  35409  poimirlem10  35410  poimirlem11  35411  poimirlem12  35412  poimirlem13  35413  poimirlem14  35414  poimirlem15  35415  poimirlem16  35416  poimirlem17  35417  poimirlem18  35418  poimirlem19  35419  poimirlem20  35420  poimirlem21  35421  poimirlem22  35422  poimirlem26  35426  mblfinlem2  35438  mhphflem  39863  mhphf  39864  rencldnfilem  40214  irrapx1  40222  scottelrankd  41407  radcnvrat  41470  supminfxr  42544  fsumiunss  42658  dvnprodlem1  43029  stoweidlem15  43098  stoweidlem31  43114  fourierdlem25  43215  fourierdlem51  43240  fourierdlem79  43268  etransclem28  43345  issalgend  43419  sge0iunmptlemre  43495  hoidmvlelem2  43676  issmflem  43802  smfresal  43861  2zrngasgrp  45032  2zrngamnd  45033  2zrngacmnd  45034  2zrngagrp  45035  2zrngmsgrp  45039  2zrngALT  45040  2zrngnmlid  45041  2zrngnmlid2  45043