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 2836	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2739	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 488	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2111	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2887	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2848	. . . . . 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 3413	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2878	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  ssrab2  4028  elfvmptrab1w  7015  elfvmptrab1  7016  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  elovmpt3rab1  7675  mapfienlem1  9378  mapfienlem2  9379  mapfienlem3  9380  scottelrankd  9890  kmlem1  10156  fin1a2lem9  10413  ac6num  10484  nnind  12278  ublbneg  12985  supminf  12987  rlimrege0  15669  incexc2  15930  lcmgcdlem  16699  phisum  16885  prmgaplem5  17150  isinitoi  18091  istermoi  18092  odcl  19666  odlem2  19669  gexcl  19710  gexlem2  19712  gexdvds  19714  pgpssslw  19744  psgnfix2  21815  psgndiflemB  21816  psgndif  21818  copsgndif  21819  psrbagf  22136  psrbagleadd1  22146  resspsrmul  22193  mplbas2  22261  rhmcomulmpl  22343  mhpmulcl  22380  psdmul  22397  mptcoe1fsupp  22443  psropprmul  22465  coe1mul2  22498  cpmatpmat  22938  mptcoe1matfsupp  23030  mp2pm2mplem4  23037  chpscmat  23070  chpscmatgsumbin  23072  chpscmatgsummon  23073  txdis1cn  23864  ptcmplem3  24283  rrxmvallem  25635  mdegmullem  26306  0sgm  27383  sgmf  27384  sgmnncl  27386  fsumdvdsdiaglem  27422  fsumdvdscom  27424  dvdsppwf1o  27425  dvdsflf1o  27426  musumsum  27431  muinv  27432  sgmppw  27436  rpvmasumlem  27726  dchrmusum2  27733  dchrvmasumlem1  27734  dchrvmasum2lem  27735  dchrisum0fmul  27745  dchrisum0ff  27746  dchrisum0flblem1  27747  dchrisum0  27759  logsqvma  27781  precsexlem9  28483  usgredg2v  29690  umgrres1lem  29773  upgrres1  29776  vtxdgoddnumeven  30016  rusgrnumwwlks  30448  frgrwopreglem4  30798  frgrwopreg  30806  rabsnel  32978  nnindf  33293  cyc3evpm  33593  cycpmgcl  33596  cycpmconjslem2  33598  elrgspnsubrun  33692  nsgmgclem  33843  mplvrpmrhm  34060  ddemeas  34750  imambfm  34776  eulerpartlemgs2  34894  ballotlemfc0  35007  ballotlemfcc  35008  ballotlemirc  35046  reprf  35123  tgoldbachgnn  35170  tgoldbachgt  35174  bnj110  35370  fnrelpredd  35599  wevgblacfn  35711  weiunlem  37085  poimirlem4  38376  poimirlem5  38377  poimirlem6  38378  poimirlem7  38379  poimirlem8  38380  poimirlem9  38381  poimirlem10  38382  poimirlem11  38383  poimirlem12  38384  poimirlem13  38385  poimirlem14  38386  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem18  38390  poimirlem19  38391  poimirlem20  38392  poimirlem21  38393  poimirlem22  38394  poimirlem26  38398  mblfinlem2  38410  primrootsunit1  42966  hashscontpow1  42990  aks6d1c6lem2  43040  aks6d1c6lem3  43041  grpods  43063  rhmcomulpsr  43431  mhphflem  43445  mhphf  43446  rencldnfilem  43664  irrapx1  43672  radcnvrat  45141  supminfxr  46295  fsumiunss  46408  dvnprodlem1  46777  stoweidlem15  46846  stoweidlem31  46862  fourierdlem25  46963  fourierdlem51  46988  fourierdlem79  47016  etransclem28  47093  issalgend  47169  sge0iunmptlemre  47246  hoidmvlelem2  47427  issmflem  47558  smfresal  47619  2zrngasgrp  49164  2zrngamnd  49165  2zrngacmnd  49166  2zrngagrp  49167  2zrngmsgrp  49171  2zrngALT  49172  2zrngnmlid  49173  2zrngnmlid2  49175  dvsec  50692  dvcsc  50693  dvcot  50694