Theorem elrabi 3647

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 2176, ax-11 2192, ax-12 2213. (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 2839	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2742	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 486	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2108	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2890	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 220	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 219	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 480	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 602	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1951	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 219	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3416	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2881	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561  ∃wex 1800  [wsb 2091   ∈ wcel 2143  {cab 2741  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416

This theorem is referenced by:  ssrab2  4034  elfvmptrab1w  7004  elfvmptrab1  7005  elovmporab  7643  elovmporab1w  7644  elovmporab1  7645  elovmpt3rab1  7657  mapfienlem1  9352  mapfienlem2  9353  mapfienlem3  9354  kmlem1  10108  fin1a2lem9  10366  ac6num  10437  nnind  12229  ublbneg  12935  supminf  12937  rlimrege0  15607  incexc2  15869  lcmgcdlem  16641  phisum  16827  prmgaplem5  17092  isinitoi  18033  istermoi  18034  odcl  19577  odlem2  19580  gexcl  19621  gexlem2  19623  gexdvds  19625  pgpssslw  19655  psgnfix2  21652  psgndiflemB  21653  psgndif  21655  copsgndif  21656  psrbagf  21971  psrbagleadd1  21981  resspsrmul  22028  mplbas2  22096  rhmcomulmpl  22178  mhpmulcl  22215  psdmul  22232  mptcoe1fsupp  22278  psropprmul  22300  coe1mul2  22333  cpmatpmat  22771  mptcoe1matfsupp  22863  mp2pm2mplem4  22870  chpscmat  22903  chpscmatgsumbin  22905  chpscmatgsummon  22906  txdis1cn  23696  ptcmplem3  24115  rrxmvallem  25467  mdegmullem  26139  0sgm  27209  sgmf  27210  sgmnncl  27212  fsumdvdsdiaglem  27248  fsumdvdscom  27250  dvdsppwf1o  27251  dvdsflf1o  27252  musumsum  27257  muinv  27258  sgmppw  27262  rpvmasumlem  27552  dchrmusum2  27559  dchrvmasumlem1  27560  dchrvmasum2lem  27561  dchrisum0fmul  27571  dchrisum0ff  27572  dchrisum0flblem1  27573  dchrisum0  27585  logsqvma  27607  precsexlem9  28309  usgredg2v  29429  umgrres1lem  29512  upgrres1  29515  vtxdgoddnumeven  29755  rusgrnumwwlks  30178  frgrwopreglem4  30518  frgrwopreg  30526  rabsnel  32700  nnindf  33023  cyc3evpm  33331  cycpmgcl  33334  cycpmconjslem2  33336  elrgspnsubrun  33431  nsgmgclem  33598  mplvrpmrhm  33845  ddemeas  34534  imambfm  34560  eulerpartlemgs2  34678  ballotlemfc0  34791  ballotlemfcc  34792  ballotlemirc  34830  reprf  34907  tgoldbachgnn  34954  tgoldbachgt  34958  bnj110  35154  fnrelpredd  35388  wevgblacfn  35455  weiunlem  36824  poimirlem4  38124  poimirlem5  38125  poimirlem6  38126  poimirlem7  38127  poimirlem8  38128  poimirlem9  38129  poimirlem10  38130  poimirlem11  38131  poimirlem12  38132  poimirlem13  38133  poimirlem14  38134  poimirlem15  38135  poimirlem16  38136  poimirlem17  38137  poimirlem18  38138  poimirlem19  38139  poimirlem20  38140  poimirlem21  38141  poimirlem22  38142  poimirlem26  38146  mblfinlem2  38158  primrootsunit1  42715  hashscontpow1  42739  aks6d1c6lem2  42789  aks6d1c6lem3  42790  grpods  42812  rhmcomulpsr  43165  mhphflem  43179  mhphf  43180  rencldnfilem  43398  irrapx1  43406  scottelrankd  44824  radcnvrat  44891  supminfxr  46039  fsumiunss  46152  dvnprodlem1  46521  stoweidlem15  46590  stoweidlem31  46606  fourierdlem25  46707  fourierdlem51  46732  fourierdlem79  46760  etransclem28  46837  issalgend  46913  sge0iunmptlemre  46990  hoidmvlelem2  47171  issmflem  47302  smfresal  47363  2zrngasgrp  48869  2zrngamnd  48870  2zrngacmnd  48871  2zrngagrp  48872  2zrngmsgrp  48876  2zrngALT  48877  2zrngnmlid  48878  2zrngnmlid2  48880