Theorem elrabi 3643

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 2813	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2716	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2080	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2864	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2825	. . . . . 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 3401	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2855	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401

This theorem is referenced by:  ssrab2  4033  elfvmptrab1w  6970  elfvmptrab1  6971  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  elovmpt3rab1  7620  mapfienlem1  9312  mapfienlem2  9313  mapfienlem3  9314  kmlem1  10065  fin1a2lem9  10322  ac6num  10393  nnind  12167  ublbneg  12850  supminf  12852  rlimrege0  15506  incexc2  15765  lcmgcdlem  16537  phisum  16722  prmgaplem5  16987  isinitoi  17927  istermoi  17928  odcl  19469  odlem2  19472  gexcl  19513  gexlem2  19515  gexdvds  19517  pgpssslw  19547  psgnfix2  21558  psgndiflemB  21559  psgndif  21561  copsgndif  21562  psrbagf  21878  psrbagleadd1  21888  resspsrmul  21935  mplbas2  22001  mhpmulcl  22096  psdmul  22113  mptcoe1fsupp  22160  psropprmul  22182  coe1mul2  22215  rhmcomulmpl  22330  cpmatpmat  22658  mptcoe1matfsupp  22750  mp2pm2mplem4  22757  chpscmat  22790  chpscmatgsumbin  22792  chpscmatgsummon  22793  txdis1cn  23583  ptcmplem3  24002  rrxmvallem  25364  mdegmullem  26043  0sgm  27114  sgmf  27115  sgmnncl  27117  fsumdvdsdiaglem  27153  fsumdvdscom  27155  dvdsppwf1o  27156  dvdsflf1o  27157  musumsum  27162  muinv  27163  sgmppw  27168  rpvmasumlem  27458  dchrmusum2  27465  dchrvmasumlem1  27466  dchrvmasum2lem  27467  dchrisum0fmul  27477  dchrisum0ff  27478  dchrisum0flblem1  27479  dchrisum0  27491  logsqvma  27513  precsexlem9  28215  usgredg2v  29304  umgrres1lem  29387  upgrres1  29390  vtxdgoddnumeven  29631  rusgrnumwwlks  30054  frgrwopreglem4  30394  frgrwopreg  30402  rabsnel  32578  nnindf  32902  cyc3evpm  33234  cycpmgcl  33237  cycpmconjslem2  33239  elrgspnsubrun  33333  nsgmgclem  33494  mplvrpmrhm  33714  ddemeas  34395  imambfm  34421  eulerpartlemgs2  34539  ballotlemfc0  34652  ballotlemfcc  34653  ballotlemirc  34691  reprf  34771  tgoldbachgnn  34818  tgoldbachgt  34822  bnj110  35016  fnrelpredd  35249  wevgblacfn  35305  weiunlem  36659  poimirlem4  37827  poimirlem5  37828  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem9  37832  poimirlem10  37833  poimirlem11  37834  poimirlem12  37835  poimirlem13  37836  poimirlem14  37837  poimirlem15  37838  poimirlem16  37839  poimirlem17  37840  poimirlem18  37841  poimirlem19  37842  poimirlem20  37843  poimirlem21  37844  poimirlem22  37845  poimirlem26  37849  mblfinlem2  37861  primrootsunit1  42419  hashscontpow1  42443  aks6d1c6lem2  42493  aks6d1c6lem3  42494  grpods  42516  rhmcomulpsr  42871  mhphflem  42906  mhphf  42907  rencldnfilem  43129  irrapx1  43137  scottelrankd  44555  radcnvrat  44622  supminfxr  45775  fsumiunss  45888  dvnprodlem1  46257  stoweidlem15  46326  stoweidlem31  46342  fourierdlem25  46443  fourierdlem51  46468  fourierdlem79  46496  etransclem28  46573  issalgend  46649  sge0iunmptlemre  46726  hoidmvlelem2  46907  issmflem  47038  smfresal  47099  2zrngasgrp  48559  2zrngamnd  48560  2zrngacmnd  48561  2zrngagrp  48562  2zrngmsgrp  48566  2zrngALT  48567  2zrngnmlid  48568  2zrngnmlid2  48570