Theorem elrabi 3630

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 2147, ax-11 2163, ax-12 2185. (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 2715	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2080	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2863	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 594	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1932	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3390	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2854	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781  [wsb 2068   ∈ wcel 2114  {cab 2714  {crab 3389

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  ssrab2  4020  elfvmptrab1w  6975  elfvmptrab1  6976  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  elovmpt3rab1  7627  mapfienlem1  9318  mapfienlem2  9319  mapfienlem3  9320  kmlem1  10073  fin1a2lem9  10330  ac6num  10401  nnind  12192  ublbneg  12883  supminf  12885  rlimrege0  15541  incexc2  15803  lcmgcdlem  16575  phisum  16761  prmgaplem5  17026  isinitoi  17966  istermoi  17967  odcl  19511  odlem2  19514  gexcl  19555  gexlem2  19557  gexdvds  19559  pgpssslw  19589  psgnfix2  21579  psgndiflemB  21580  psgndif  21582  copsgndif  21583  psrbagf  21898  psrbagleadd1  21908  resspsrmul  21954  mplbas2  22020  mhpmulcl  22115  psdmul  22132  mptcoe1fsupp  22179  psropprmul  22201  coe1mul2  22234  rhmcomulmpl  22347  cpmatpmat  22675  mptcoe1matfsupp  22767  mp2pm2mplem4  22774  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  txdis1cn  23600  ptcmplem3  24019  rrxmvallem  25371  mdegmullem  26043  0sgm  27107  sgmf  27108  sgmnncl  27110  fsumdvdsdiaglem  27146  fsumdvdscom  27148  dvdsppwf1o  27149  dvdsflf1o  27150  musumsum  27155  muinv  27156  sgmppw  27160  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrisum0fmul  27469  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0  27483  logsqvma  27505  precsexlem9  28207  usgredg2v  29296  umgrres1lem  29379  upgrres1  29382  vtxdgoddnumeven  29622  rusgrnumwwlks  30045  frgrwopreglem4  30385  frgrwopreg  30393  rabsnel  32570  nnindf  32893  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  elrgspnsubrun  33310  nsgmgclem  33471  mplvrpmrhm  33691  ddemeas  34380  imambfm  34406  eulerpartlemgs2  34524  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemirc  34676  reprf  34756  tgoldbachgnn  34803  tgoldbachgt  34807  bnj110  35000  fnrelpredd  35234  wevgblacfn  35291  weiunlem  36645  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem26  37967  mblfinlem2  37979  primrootsunit1  42536  hashscontpow1  42560  aks6d1c6lem2  42610  aks6d1c6lem3  42611  grpods  42633  rhmcomulpsr  42994  mhphflem  43029  mhphf  43030  rencldnfilem  43248  irrapx1  43256  scottelrankd  44674  radcnvrat  44741  supminfxr  45892  fsumiunss  46005  dvnprodlem1  46374  stoweidlem15  46443  stoweidlem31  46459  fourierdlem25  46560  fourierdlem51  46585  fourierdlem79  46613  etransclem28  46690  issalgend  46766  sge0iunmptlemre  46843  hoidmvlelem2  47024  issmflem  47155  smfresal  47216  2zrngasgrp  48722  2zrngamnd  48723  2zrngacmnd  48724  2zrngagrp  48725  2zrngmsgrp  48729  2zrngALT  48730  2zrngnmlid  48731  2zrngnmlid2  48733