Theorem elrabi 3611

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 2139, ax-11 2156, ax-12 2173. (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 2818	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2716	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2078	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2866	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 217	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 216	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 592	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1934	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 216	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3072	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2857	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1783  [wsb 2068   ∈ wcel 2108  {cab 2715  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  ssrab2  4009  elfvmptrab1w  6883  elfvmptrab1  6884  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  elovmpt3rab1  7507  mapfienlem1  9094  mapfienlem2  9095  mapfienlem3  9096  kmlem1  9837  fin1a2lem9  10095  ac6num  10166  nnind  11921  ublbneg  12602  supminf  12604  rlimrege0  15216  incexc2  15478  lcmgcdlem  16239  phisum  16419  prmgaplem5  16684  isinitoi  17630  istermoi  17631  odcl  19059  odlem2  19062  gexcl  19100  gexlem2  19102  gexdvds  19104  pgpssslw  19134  psgnfix2  20716  psgndiflemB  20717  psgndif  20719  copsgndif  20720  psrbagf  21031  resspsrmul  21096  mplbas2  21153  mhpmulcl  21249  mptcoe1fsupp  21296  psropprmul  21319  coe1mul2  21350  cpmatpmat  21767  mptcoe1matfsupp  21859  mp2pm2mplem4  21866  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  txdis1cn  22694  ptcmplem3  23113  rrxmvallem  24473  mdegmullem  25148  0sgm  26198  sgmf  26199  sgmnncl  26201  fsumdvdsdiaglem  26237  fsumdvdscom  26239  dvdsppwf1o  26240  dvdsflf1o  26241  musumsum  26246  muinv  26247  sgmppw  26250  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrisum0fmul  26559  dchrisum0ff  26560  dchrisum0flblem1  26561  dchrisum0  26573  logsqvma  26595  usgredg2v  27497  umgrres1lem  27580  upgrres1  27583  vtxdgoddnumeven  27823  rusgrnumwwlks  28240  frgrwopreglem4  28580  frgrwopreg  28588  rabsnel  30748  nnindf  31035  cyc3evpm  31319  cycpmgcl  31322  cycpmconjslem2  31324  nsgmgclem  31498  ddemeas  32104  imambfm  32129  eulerpartlemgs2  32247  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemirc  32398  reprf  32492  tgoldbachgnn  32539  tgoldbachgt  32543  bnj110  32738  fnrelpredd  32961  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem26  35730  mblfinlem2  35742  mhphflem  40207  mhphf  40208  rencldnfilem  40558  irrapx1  40566  scottelrankd  41754  radcnvrat  41821  supminfxr  42894  fsumiunss  43006  dvnprodlem1  43377  stoweidlem15  43446  stoweidlem31  43462  fourierdlem25  43563  fourierdlem51  43588  fourierdlem79  43616  etransclem28  43693  issalgend  43767  sge0iunmptlemre  43843  hoidmvlelem2  44024  issmflem  44150  smfresal  44209  2zrngasgrp  45386  2zrngamnd  45387  2zrngacmnd  45388  2zrngagrp  45389  2zrngmsgrp  45393  2zrngALT  45394  2zrngnmlid  45395  2zrngnmlid2  45397