Theorem elrabi 3703

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 2141, 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 2820	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2718	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2074	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2871	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2832	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 592	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1929	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3444	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2862	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∃wex 1777  [wsb 2064   ∈ wcel 2108  {cab 2717  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  ssrab2  4103  elfvmptrab1w  7056  elfvmptrab1  7057  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  elovmpt3rab1  7710  mapfienlem1  9474  mapfienlem2  9475  mapfienlem3  9476  kmlem1  10220  fin1a2lem9  10477  ac6num  10548  nnind  12311  ublbneg  12998  supminf  13000  rlimrege0  15625  incexc2  15886  lcmgcdlem  16653  phisum  16837  prmgaplem5  17102  isinitoi  18066  istermoi  18067  odcl  19578  odlem2  19581  gexcl  19622  gexlem2  19624  gexdvds  19626  pgpssslw  19656  psgnfix2  21640  psgndiflemB  21641  psgndif  21643  copsgndif  21644  psrbagf  21961  psrbagleadd1  21971  resspsrmul  22019  mplbas2  22083  mhpmulcl  22176  psdmul  22193  mptcoe1fsupp  22238  psropprmul  22260  coe1mul2  22293  rhmcomulmpl  22407  cpmatpmat  22737  mptcoe1matfsupp  22829  mp2pm2mplem4  22836  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  txdis1cn  23664  ptcmplem3  24083  rrxmvallem  25457  mdegmullem  26137  0sgm  27205  sgmf  27206  sgmnncl  27208  fsumdvdsdiaglem  27244  fsumdvdscom  27246  dvdsppwf1o  27247  dvdsflf1o  27248  musumsum  27253  muinv  27254  sgmppw  27259  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrisum0fmul  27568  dchrisum0ff  27569  dchrisum0flblem1  27570  dchrisum0  27582  logsqvma  27604  precsexlem9  28257  usgredg2v  29262  umgrres1lem  29345  upgrres1  29348  vtxdgoddnumeven  29589  rusgrnumwwlks  30007  frgrwopreglem4  30347  frgrwopreg  30355  rabsnel  32528  nnindf  32823  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  nsgmgclem  33404  ddemeas  34200  imambfm  34227  eulerpartlemgs2  34345  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemirc  34496  reprf  34589  tgoldbachgnn  34636  tgoldbachgt  34640  bnj110  34834  fnrelpredd  35065  wevgblacfn  35076  weiunlem2  36429  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem26  37606  mblfinlem2  37618  primrootsunit1  42054  hashscontpow1  42078  aks6d1c6lem2  42128  aks6d1c6lem3  42129  grpods  42151  rhmcomulpsr  42506  mhphflem  42551  mhphf  42552  rencldnfilem  42776  irrapx1  42784  scottelrankd  44216  radcnvrat  44283  supminfxr  45379  fsumiunss  45496  dvnprodlem1  45867  stoweidlem15  45936  stoweidlem31  45952  fourierdlem25  46053  fourierdlem51  46078  fourierdlem79  46106  etransclem28  46183  issalgend  46259  sge0iunmptlemre  46336  hoidmvlelem2  46517  issmflem  46648  smfresal  46709  2zrngasgrp  47969  2zrngamnd  47970  2zrngacmnd  47971  2zrngagrp  47972  2zrngmsgrp  47976  2zrngALT  47977  2zrngnmlid  47978  2zrngnmlid2  47980