Theorem elrabi 3651

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 2142, ax-11 2158, ax-12 2178. (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 2804	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2708	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2075	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2855	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2816	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1930	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3403	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2846	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2707  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  ssrab2  4039  elfvmptrab1w  6977  elfvmptrab1  6978  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  elovmpt3rab1  7629  mapfienlem1  9332  mapfienlem2  9333  mapfienlem3  9334  kmlem1  10080  fin1a2lem9  10337  ac6num  10408  nnind  12180  ublbneg  12868  supminf  12870  rlimrege0  15521  incexc2  15780  lcmgcdlem  16552  phisum  16737  prmgaplem5  17002  isinitoi  17941  istermoi  17942  odcl  19450  odlem2  19453  gexcl  19494  gexlem2  19496  gexdvds  19498  pgpssslw  19528  psgnfix2  21541  psgndiflemB  21542  psgndif  21544  copsgndif  21545  psrbagf  21860  psrbagleadd1  21870  resspsrmul  21918  mplbas2  21982  mhpmulcl  22069  psdmul  22086  mptcoe1fsupp  22133  psropprmul  22155  coe1mul2  22188  rhmcomulmpl  22302  cpmatpmat  22630  mptcoe1matfsupp  22722  mp2pm2mplem4  22729  chpscmat  22762  chpscmatgsumbin  22764  chpscmatgsummon  22765  txdis1cn  23555  ptcmplem3  23974  rrxmvallem  25337  mdegmullem  26016  0sgm  27087  sgmf  27088  sgmnncl  27090  fsumdvdsdiaglem  27126  fsumdvdscom  27128  dvdsppwf1o  27129  dvdsflf1o  27130  musumsum  27135  muinv  27136  sgmppw  27141  rpvmasumlem  27431  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2lem  27440  dchrisum0fmul  27450  dchrisum0ff  27451  dchrisum0flblem1  27452  dchrisum0  27464  logsqvma  27486  precsexlem9  28157  usgredg2v  29207  umgrres1lem  29290  upgrres1  29293  vtxdgoddnumeven  29534  rusgrnumwwlks  29954  frgrwopreglem4  30294  frgrwopreg  30302  rabsnel  32479  nnindf  32794  cyc3evpm  33122  cycpmgcl  33125  cycpmconjslem2  33127  elrgspnsubrun  33216  nsgmgclem  33375  ddemeas  34219  imambfm  34246  eulerpartlemgs2  34364  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemirc  34516  reprf  34596  tgoldbachgnn  34643  tgoldbachgt  34647  bnj110  34841  fnrelpredd  35072  wevgblacfn  35089  weiunlem2  36444  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem26  37633  mblfinlem2  37645  primrootsunit1  42078  hashscontpow1  42102  aks6d1c6lem2  42152  aks6d1c6lem3  42153  grpods  42175  rhmcomulpsr  42532  mhphflem  42577  mhphf  42578  rencldnfilem  42801  irrapx1  42809  scottelrankd  44229  radcnvrat  44296  supminfxr  45453  fsumiunss  45566  dvnprodlem1  45937  stoweidlem15  46006  stoweidlem31  46022  fourierdlem25  46123  fourierdlem51  46148  fourierdlem79  46176  etransclem28  46253  issalgend  46329  sge0iunmptlemre  46406  hoidmvlelem2  46587  issmflem  46718  smfresal  46779  2zrngasgrp  48227  2zrngamnd  48228  2zrngacmnd  48229  2zrngagrp  48230  2zrngmsgrp  48234  2zrngALT  48235  2zrngnmlid  48236  2zrngnmlid2  48238