Theorem elrabi 3657

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 2142, 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 2805	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2709	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2075	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2856	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2817	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1930	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3409	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2847	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2708  {crab 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  ssrab2  4046  elfvmptrab1w  6998  elfvmptrab1  6999  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  elovmpt3rab1  7652  mapfienlem1  9363  mapfienlem2  9364  mapfienlem3  9365  kmlem1  10111  fin1a2lem9  10368  ac6num  10439  nnind  12211  ublbneg  12899  supminf  12901  rlimrege0  15552  incexc2  15811  lcmgcdlem  16583  phisum  16768  prmgaplem5  17033  isinitoi  17968  istermoi  17969  odcl  19473  odlem2  19476  gexcl  19517  gexlem2  19519  gexdvds  19521  pgpssslw  19551  psgnfix2  21515  psgndiflemB  21516  psgndif  21518  copsgndif  21519  psrbagf  21834  psrbagleadd1  21844  resspsrmul  21892  mplbas2  21956  mhpmulcl  22043  psdmul  22060  mptcoe1fsupp  22107  psropprmul  22129  coe1mul2  22162  rhmcomulmpl  22276  cpmatpmat  22604  mptcoe1matfsupp  22696  mp2pm2mplem4  22703  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  txdis1cn  23529  ptcmplem3  23948  rrxmvallem  25311  mdegmullem  25990  0sgm  27061  sgmf  27062  sgmnncl  27064  fsumdvdsdiaglem  27100  fsumdvdscom  27102  dvdsppwf1o  27103  dvdsflf1o  27104  musumsum  27109  muinv  27110  sgmppw  27115  rpvmasumlem  27405  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrisum0fmul  27424  dchrisum0ff  27425  dchrisum0flblem1  27426  dchrisum0  27438  logsqvma  27460  precsexlem9  28124  usgredg2v  29161  umgrres1lem  29244  upgrres1  29247  vtxdgoddnumeven  29488  rusgrnumwwlks  29911  frgrwopreglem4  30251  frgrwopreg  30259  rabsnel  32436  nnindf  32751  cyc3evpm  33114  cycpmgcl  33117  cycpmconjslem2  33119  elrgspnsubrun  33207  nsgmgclem  33389  ddemeas  34233  imambfm  34260  eulerpartlemgs2  34378  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemirc  34530  reprf  34610  tgoldbachgnn  34657  tgoldbachgt  34661  bnj110  34855  fnrelpredd  35086  wevgblacfn  35103  weiunlem2  36458  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem26  37647  mblfinlem2  37659  primrootsunit1  42092  hashscontpow1  42116  aks6d1c6lem2  42166  aks6d1c6lem3  42167  grpods  42189  rhmcomulpsr  42546  mhphflem  42591  mhphf  42592  rencldnfilem  42815  irrapx1  42823  scottelrankd  44243  radcnvrat  44310  supminfxr  45467  fsumiunss  45580  dvnprodlem1  45951  stoweidlem15  46020  stoweidlem31  46036  fourierdlem25  46137  fourierdlem51  46162  fourierdlem79  46190  etransclem28  46267  issalgend  46343  sge0iunmptlemre  46420  hoidmvlelem2  46601  issmflem  46732  smfresal  46793  2zrngasgrp  48238  2zrngamnd  48239  2zrngacmnd  48240  2zrngagrp  48241  2zrngmsgrp  48245  2zrngALT  48246  2zrngnmlid  48247  2zrngnmlid2  48249