Theorem elrabi 3631

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 3391	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2855	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 3391

This theorem is referenced by:  ssrab2  4021  elfvmptrab1w  6971  elfvmptrab1  6972  elovmporab  7608  elovmporab1w  7609  elovmporab1  7610  elovmpt3rab1  7622  mapfienlem1  9313  mapfienlem2  9314  mapfienlem3  9315  kmlem1  10068  fin1a2lem9  10325  ac6num  10396  nnind  12187  ublbneg  12878  supminf  12880  rlimrege0  15536  incexc2  15798  lcmgcdlem  16570  phisum  16756  prmgaplem5  17021  isinitoi  17961  istermoi  17962  odcl  19506  odlem2  19509  gexcl  19550  gexlem2  19552  gexdvds  19554  pgpssslw  19584  psgnfix2  21593  psgndiflemB  21594  psgndif  21596  copsgndif  21597  psrbagf  21912  psrbagleadd1  21922  resspsrmul  21968  mplbas2  22034  mhpmulcl  22129  psdmul  22146  mptcoe1fsupp  22193  psropprmul  22215  coe1mul2  22248  rhmcomulmpl  22361  cpmatpmat  22689  mptcoe1matfsupp  22781  mp2pm2mplem4  22788  chpscmat  22821  chpscmatgsumbin  22823  chpscmatgsummon  22824  txdis1cn  23614  ptcmplem3  24033  rrxmvallem  25385  mdegmullem  26057  0sgm  27125  sgmf  27126  sgmnncl  27128  fsumdvdsdiaglem  27164  fsumdvdscom  27166  dvdsppwf1o  27167  dvdsflf1o  27168  musumsum  27173  muinv  27174  sgmppw  27178  rpvmasumlem  27468  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrisum0fmul  27487  dchrisum0ff  27488  dchrisum0flblem1  27489  dchrisum0  27501  logsqvma  27523  precsexlem9  28225  usgredg2v  29314  umgrres1lem  29397  upgrres1  29400  vtxdgoddnumeven  29641  rusgrnumwwlks  30064  frgrwopreglem4  30404  frgrwopreg  30412  rabsnel  32589  nnindf  32912  cyc3evpm  33230  cycpmgcl  33233  cycpmconjslem2  33235  elrgspnsubrun  33329  nsgmgclem  33490  mplvrpmrhm  33710  ddemeas  34400  imambfm  34426  eulerpartlemgs2  34544  ballotlemfc0  34657  ballotlemfcc  34658  ballotlemirc  34696  reprf  34776  tgoldbachgnn  34823  tgoldbachgt  34827  bnj110  35020  fnrelpredd  35254  wevgblacfn  35311  weiunlem  36665  poimirlem4  37963  poimirlem5  37964  poimirlem6  37965  poimirlem7  37966  poimirlem8  37967  poimirlem9  37968  poimirlem10  37969  poimirlem11  37970  poimirlem12  37971  poimirlem13  37972  poimirlem14  37973  poimirlem15  37974  poimirlem16  37975  poimirlem17  37976  poimirlem18  37977  poimirlem19  37978  poimirlem20  37979  poimirlem21  37980  poimirlem22  37981  poimirlem26  37985  mblfinlem2  37997  primrootsunit1  42554  hashscontpow1  42578  aks6d1c6lem2  42628  aks6d1c6lem3  42629  grpods  42651  rhmcomulpsr  43012  mhphflem  43047  mhphf  43048  rencldnfilem  43270  irrapx1  43278  scottelrankd  44696  radcnvrat  44763  supminfxr  45914  fsumiunss  46027  dvnprodlem1  46396  stoweidlem15  46465  stoweidlem31  46481  fourierdlem25  46582  fourierdlem51  46607  fourierdlem79  46635  etransclem28  46712  issalgend  46788  sge0iunmptlemre  46865  hoidmvlelem2  47046  issmflem  47177  smfresal  47238  2zrngasgrp  48738  2zrngamnd  48739  2zrngacmnd  48740  2zrngagrp  48741  2zrngmsgrp  48745  2zrngALT  48746  2zrngnmlid  48747  2zrngnmlid2  48749