Theorem elrabi 3641

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 2178, ax-11 2194, ax-12 2213. (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 2837	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2740	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 488	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2111	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2888	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2849	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 482	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 605	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1963	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3414	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2879	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812  [wsb 2099   ∈ wcel 2145  {cab 2739  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  ssrab2  4028  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  elovmpt3rab1  7681  mapfienlem1  9397  mapfienlem2  9398  mapfienlem3  9399  scottelrankd  9948  kmlem1  10229  fin1a2lem9  10486  ac6num  10557  nnind  12353  ublbneg  13060  supminf  13062  rlimrege0  15746  incexc2  16007  lcmgcdlem  16781  phisum  16968  prmgaplem5  17233  isinitoi  18174  istermoi  18175  odcl  19750  odlem2  19753  gexcl  19794  gexlem2  19796  gexdvds  19798  pgpssslw  19828  psgnfix2  21905  psgndiflemB  21906  psgndif  21908  copsgndif  21909  psrbagf  22226  psrbagleadd1  22236  resspsrmul  22283  mplbas2  22351  rhmcomulmpl  22433  mhpmulcl  22470  psdmul  22487  mptcoe1fsupp  22533  psropprmul  22555  coe1mul2  22588  cpmatpmat  23028  mptcoe1matfsupp  23120  mp2pm2mplem4  23127  chpscmat  23160  chpscmatgsumbin  23162  chpscmatgsummon  23163  txdis1cn  23954  ptcmplem3  24373  rrxmvallem  25725  mdegmullem  26396  0sgm  27471  sgmf  27472  sgmnncl  27474  fsumdvdsdiaglem  27510  fsumdvdscom  27512  dvdsppwf1o  27513  dvdsflf1o  27514  musumsum  27519  muinv  27520  sgmppw  27524  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasumlem1  27822  dchrvmasum2lem  27823  dchrisum0fmul  27833  dchrisum0ff  27834  dchrisum0flblem1  27835  dchrisum0  27847  logsqvma  27869  precsexlem9  28601  usgredg2v  29808  umgrres1lem  29891  upgrres1  29894  vtxdgoddnumeven  30134  rusgrnumwwlks  30566  frgrwopreglem4  30916  frgrwopreg  30924  rabsnel  33096  nnindf  33411  cyc3evpm  33711  cycpmgcl  33714  cycpmconjslem2  33716  elrgspnsubrun  33810  nsgmgclem  33962  mplvrpmrhm  34179  ddemeas  34869  imambfm  34894  eulerpartlemgs2  35012  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemirc  35164  reprf  35241  tgoldbachgnn  35288  tgoldbachgt  35292  bnj110  35488  fnrelpredd  35720  wevgblacfn  35890  weiunlem  37251  poimirlem4  38542  poimirlem5  38543  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem9  38547  poimirlem10  38548  poimirlem11  38549  poimirlem12  38550  poimirlem13  38551  poimirlem14  38552  poimirlem15  38553  poimirlem16  38554  poimirlem17  38555  poimirlem18  38556  poimirlem19  38557  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem26  38564  mblfinlem2  38576  primrootsunit1  43147  hashscontpow1  43171  aks6d1c6lem2  43221  aks6d1c6lem3  43222  grpods  43244  rhmcomulpsr  43610  mhphflem  43624  mhphf  43625  rencldnfilem  43826  irrapx1  43834  radcnvrat  45297  supminfxr  46473  fsumiunss  46586  dvnprodlem1  46955  stoweidlem15  47024  stoweidlem31  47040  fourierdlem25  47141  fourierdlem51  47166  fourierdlem79  47194  etransclem28  47271  issalgend  47347  sge0iunmptlemre  47424  hoidmvlelem2  47605  issmflem  47736  smfresal  47797  2zrngasgrp  49342  2zrngamnd  49343  2zrngacmnd  49344  2zrngagrp  49345  2zrngmsgrp  49349  2zrngALT  49350  2zrngnmlid  49351  2zrngnmlid2  49353  dvsec  50855  dvcsc  50856  dvcot  50857