Theorem elrabi 3648

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 2179, ax-11 2195, ax-12 2216. (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 2841	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2744	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 488	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2111	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2892	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2853	. . . . . 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 3419	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2883	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419

This theorem is used by:  ssrab2  4035  elfvmptrab1w  7021  elfvmptrab1  7022  elovmporab  7666  elovmporab1w  7667  elovmporab1  7668  elovmpt3rab1  7680  mapfienlem1  9372  mapfienlem2  9373  mapfienlem3  9374  scottelrankd  9884  kmlem1  10150  fin1a2lem9  10407  ac6num  10478  nnind  12270  ublbneg  12977  supminf  12979  rlimrege0  15658  incexc2  15919  lcmgcdlem  16690  phisum  16876  prmgaplem5  17141  isinitoi  18082  istermoi  18083  odcl  19654  odlem2  19657  gexcl  19698  gexlem2  19700  gexdvds  19702  pgpssslw  19732  psgnfix2  21803  psgndiflemB  21804  psgndif  21806  copsgndif  21807  psrbagf  22122  psrbagleadd1  22132  resspsrmul  22179  mplbas2  22247  rhmcomulmpl  22329  mhpmulcl  22366  psdmul  22383  mptcoe1fsupp  22429  psropprmul  22451  coe1mul2  22484  cpmatpmat  22921  mptcoe1matfsupp  23013  mp2pm2mplem4  23020  chpscmat  23053  chpscmatgsumbin  23055  chpscmatgsummon  23056  txdis1cn  23847  ptcmplem3  24266  rrxmvallem  25618  mdegmullem  26290  0sgm  27363  sgmf  27364  sgmnncl  27366  fsumdvdsdiaglem  27402  fsumdvdscom  27404  dvdsppwf1o  27405  dvdsflf1o  27406  musumsum  27411  muinv  27412  sgmppw  27416  rpvmasumlem  27706  dchrmusum2  27713  dchrvmasumlem1  27714  dchrvmasum2lem  27715  dchrisum0fmul  27725  dchrisum0ff  27726  dchrisum0flblem1  27727  dchrisum0  27739  logsqvma  27761  precsexlem9  28463  usgredg2v  29639  umgrres1lem  29722  upgrres1  29725  vtxdgoddnumeven  29965  rusgrnumwwlks  30397  frgrwopreglem4  30741  frgrwopreg  30749  rabsnel  32921  nnindf  33238  cyc3evpm  33538  cycpmgcl  33541  cycpmconjslem2  33543  elrgspnsubrun  33637  nsgmgclem  33788  mplvrpmrhm  34005  ddemeas  34695  imambfm  34721  eulerpartlemgs2  34839  ballotlemfc0  34952  ballotlemfcc  34953  ballotlemirc  34991  reprf  35068  tgoldbachgnn  35115  tgoldbachgt  35119  bnj110  35315  fnrelpredd  35544  wevgblacfn  35656  weiunlem  37035  poimirlem4  38336  poimirlem5  38337  poimirlem6  38338  poimirlem7  38339  poimirlem8  38340  poimirlem9  38341  poimirlem10  38342  poimirlem11  38343  poimirlem12  38344  poimirlem13  38345  poimirlem14  38346  poimirlem15  38347  poimirlem16  38348  poimirlem17  38349  poimirlem18  38350  poimirlem19  38351  poimirlem20  38352  poimirlem21  38353  poimirlem22  38354  poimirlem26  38358  mblfinlem2  38370  primrootsunit1  42926  hashscontpow1  42950  aks6d1c6lem2  43000  aks6d1c6lem3  43001  grpods  43023  rhmcomulpsr  43391  mhphflem  43405  mhphf  43406  rencldnfilem  43624  irrapx1  43632  radcnvrat  45101  supminfxr  46255  fsumiunss  46368  dvnprodlem1  46737  stoweidlem15  46806  stoweidlem31  46822  fourierdlem25  46923  fourierdlem51  46948  fourierdlem79  46976  etransclem28  47053  issalgend  47129  sge0iunmptlemre  47206  hoidmvlelem2  47387  issmflem  47518  smfresal  47579  2zrngasgrp  49087  2zrngamnd  49088  2zrngacmnd  49089  2zrngagrp  49090  2zrngmsgrp  49094  2zrngALT  49095  2zrngnmlid  49096  2zrngnmlid2  49098