Theorem elrabi 3625

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 2152, ax-11 2168, ax-12 2189. (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 2815	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2718	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 483	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2085	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2866	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 219	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 218	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 477	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 599	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1937	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 218	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3392	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2857	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ∃wex 1786  [wsb 2073   ∈ wcel 2119  {cab 2717  {crab 3391

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392

This theorem is referenced by:  ssrab2  4012  elfvmptrab1w  6964  elfvmptrab1  6965  elovmporab  7603  elovmporab1w  7604  elovmporab1  7605  elovmpt3rab1  7617  mapfienlem1  9309  mapfienlem2  9310  mapfienlem3  9311  kmlem1  10065  fin1a2lem9  10322  ac6num  10393  nnind  12184  ublbneg  12875  supminf  12877  rlimrege0  15533  incexc2  15795  lcmgcdlem  16567  phisum  16753  prmgaplem5  17018  isinitoi  17958  istermoi  17959  odcl  19503  odlem2  19506  gexcl  19547  gexlem2  19549  gexdvds  19551  pgpssslw  19581  psgnfix2  21575  psgndiflemB  21576  psgndif  21578  copsgndif  21579  psrbagf  21894  psrbagleadd1  21904  resspsrmul  21951  mplbas2  22019  rhmcomulmpl  22101  mhpmulcl  22138  psdmul  22155  mptcoe1fsupp  22201  psropprmul  22223  coe1mul2  22256  cpmatpmat  22694  mptcoe1matfsupp  22786  mp2pm2mplem4  22793  chpscmat  22826  chpscmatgsumbin  22828  chpscmatgsummon  22829  txdis1cn  23619  ptcmplem3  24038  rrxmvallem  25390  mdegmullem  26062  0sgm  27126  sgmf  27127  sgmnncl  27129  fsumdvdsdiaglem  27165  fsumdvdscom  27167  dvdsppwf1o  27168  dvdsflf1o  27169  musumsum  27174  muinv  27175  sgmppw  27179  rpvmasumlem  27469  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrisum0fmul  27488  dchrisum0ff  27489  dchrisum0flblem1  27490  dchrisum0  27502  logsqvma  27524  precsexlem9  28226  usgredg2v  29315  umgrres1lem  29398  upgrres1  29401  vtxdgoddnumeven  29641  rusgrnumwwlks  30064  frgrwopreglem4  30404  frgrwopreg  30412  rabsnel  32589  nnindf  32913  cyc3evpm  33232  cycpmgcl  33235  cycpmconjslem2  33237  elrgspnsubrun  33331  nsgmgclem  33495  mplvrpmrhm  33740  ddemeas  34429  imambfm  34455  eulerpartlemgs2  34573  ballotlemfc0  34686  ballotlemfcc  34687  ballotlemirc  34725  reprf  34805  tgoldbachgnn  34852  tgoldbachgt  34856  bnj110  35049  fnrelpredd  35281  wevgblacfn  35346  weiunlem  36700  poimirlem4  38000  poimirlem5  38001  poimirlem6  38002  poimirlem7  38003  poimirlem8  38004  poimirlem9  38005  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem13  38009  poimirlem14  38010  poimirlem15  38011  poimirlem16  38012  poimirlem17  38013  poimirlem18  38014  poimirlem19  38015  poimirlem20  38016  poimirlem21  38017  poimirlem22  38018  poimirlem26  38022  mblfinlem2  38034  primrootsunit1  42591  hashscontpow1  42615  aks6d1c6lem2  42665  aks6d1c6lem3  42666  grpods  42688  rhmcomulpsr  43041  mhphflem  43055  mhphf  43056  rencldnfilem  43274  irrapx1  43282  scottelrankd  44700  radcnvrat  44767  supminfxr  45915  fsumiunss  46028  dvnprodlem1  46397  stoweidlem15  46466  stoweidlem31  46482  fourierdlem25  46583  fourierdlem51  46608  fourierdlem79  46636  etransclem28  46713  issalgend  46789  sge0iunmptlemre  46866  hoidmvlelem2  47047  issmflem  47178  smfresal  47239  2zrngasgrp  48745  2zrngamnd  48746  2zrngacmnd  48747  2zrngagrp  48748  2zrngmsgrp  48752  2zrngALT  48753  2zrngnmlid  48754  2zrngnmlid2  48756