Theorem elrabi 3676

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 2137, ax-11 2154, ax-12 2171. (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 2811	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2710	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 483	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2077	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2860	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 217	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 216	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2821	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 477	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1933	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 216	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3433	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2851	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781  [wsb 2067   ∈ wcel 2106  {cab 2709  {crab 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433

This theorem is referenced by:  ssrab2  4076  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7648  elovmporab1w  7649  elovmporab1  7650  elovmpt3rab1  7662  mapfienlem1  9396  mapfienlem2  9397  mapfienlem3  9398  kmlem1  10141  fin1a2lem9  10399  ac6num  10470  nnind  12226  ublbneg  12913  supminf  12915  rlimrege0  15519  incexc2  15780  lcmgcdlem  16539  phisum  16719  prmgaplem5  16984  isinitoi  17945  istermoi  17946  odcl  19398  odlem2  19401  gexcl  19442  gexlem2  19444  gexdvds  19446  pgpssslw  19476  psgnfix2  21143  psgndiflemB  21144  psgndif  21146  copsgndif  21147  psrbagf  21462  resspsrmul  21528  mplbas2  21588  mhpmulcl  21683  mptcoe1fsupp  21730  psropprmul  21751  coe1mul2  21782  cpmatpmat  22203  mptcoe1matfsupp  22295  mp2pm2mplem4  22302  chpscmat  22335  chpscmatgsumbin  22337  chpscmatgsummon  22338  txdis1cn  23130  ptcmplem3  23549  rrxmvallem  24912  mdegmullem  25587  0sgm  26637  sgmf  26638  sgmnncl  26640  fsumdvdsdiaglem  26676  fsumdvdscom  26678  dvdsppwf1o  26679  dvdsflf1o  26680  musumsum  26685  muinv  26686  sgmppw  26689  rpvmasumlem  26979  dchrmusum2  26986  dchrvmasumlem1  26987  dchrvmasum2lem  26988  dchrisum0fmul  26998  dchrisum0ff  26999  dchrisum0flblem1  27000  dchrisum0  27012  logsqvma  27034  precsexlem9  27650  usgredg2v  28473  umgrres1lem  28556  upgrres1  28559  vtxdgoddnumeven  28799  rusgrnumwwlks  29217  frgrwopreglem4  29557  frgrwopreg  29565  rabsnel  31727  nnindf  32012  cyc3evpm  32296  cycpmgcl  32299  cycpmconjslem2  32301  nsgmgclem  32510  ddemeas  33222  imambfm  33249  eulerpartlemgs2  33367  ballotlemfc0  33479  ballotlemfcc  33480  ballotlemirc  33518  reprf  33612  tgoldbachgnn  33659  tgoldbachgt  33663  bnj110  33857  fnrelpredd  34080  poimirlem4  36480  poimirlem5  36481  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem9  36485  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem26  36502  mblfinlem2  36514  mhphflem  41165  mhphf  41166  rencldnfilem  41543  irrapx1  41551  scottelrankd  42991  radcnvrat  43058  supminfxr  44160  fsumiunss  44277  dvnprodlem1  44648  stoweidlem15  44717  stoweidlem31  44733  fourierdlem25  44834  fourierdlem51  44859  fourierdlem79  44887  etransclem28  44964  issalgend  45040  sge0iunmptlemre  45117  hoidmvlelem2  45298  issmflem  45429  smfresal  45490  2zrngasgrp  46791  2zrngamnd  46792  2zrngacmnd  46793  2zrngagrp  46794  2zrngmsgrp  46798  2zrngALT  46799  2zrngnmlid  46800  2zrngnmlid2  46802