Theorem elrabi 3678

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 2138, ax-11 2155, ax-12 2172. (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 2812	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2711	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 484	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2078	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2861	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 217	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 216	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 478	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 594	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1934	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 216	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3434	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2852	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782  [wsb 2068   ∈ wcel 2107  {cab 2710  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434

This theorem is referenced by:  ssrab2  4078  elfvmptrab1w  7025  elfvmptrab1  7026  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  elovmpt3rab1  7666  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  kmlem1  10145  fin1a2lem9  10403  ac6num  10474  nnind  12230  ublbneg  12917  supminf  12919  rlimrege0  15523  incexc2  15784  lcmgcdlem  16543  phisum  16723  prmgaplem5  16988  isinitoi  17949  istermoi  17950  odcl  19404  odlem2  19407  gexcl  19448  gexlem2  19450  gexdvds  19452  pgpssslw  19482  psgnfix2  21152  psgndiflemB  21153  psgndif  21155  copsgndif  21156  psrbagf  21471  resspsrmul  21537  mplbas2  21597  mhpmulcl  21692  mptcoe1fsupp  21739  psropprmul  21760  coe1mul2  21791  cpmatpmat  22212  mptcoe1matfsupp  22304  mp2pm2mplem4  22311  chpscmat  22344  chpscmatgsumbin  22346  chpscmatgsummon  22347  txdis1cn  23139  ptcmplem3  23558  rrxmvallem  24921  mdegmullem  25596  0sgm  26648  sgmf  26649  sgmnncl  26651  fsumdvdsdiaglem  26687  fsumdvdscom  26689  dvdsppwf1o  26690  dvdsflf1o  26691  musumsum  26696  muinv  26697  sgmppw  26700  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrisum0fmul  27009  dchrisum0ff  27010  dchrisum0flblem1  27011  dchrisum0  27023  logsqvma  27045  precsexlem9  27664  usgredg2v  28515  umgrres1lem  28598  upgrres1  28601  vtxdgoddnumeven  28841  rusgrnumwwlks  29259  frgrwopreglem4  29599  frgrwopreg  29607  rabsnel  31771  nnindf  32056  cyc3evpm  32340  cycpmgcl  32343  cycpmconjslem2  32345  nsgmgclem  32553  ddemeas  33265  imambfm  33292  eulerpartlemgs2  33410  ballotlemfc0  33522  ballotlemfcc  33523  ballotlemirc  33561  reprf  33655  tgoldbachgnn  33702  tgoldbachgt  33706  bnj110  33900  fnrelpredd  34123  poimirlem4  36540  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem8  36544  poimirlem9  36545  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem13  36549  poimirlem14  36550  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem26  36562  mblfinlem2  36574  mhphflem  41216  mhphf  41217  rencldnfilem  41606  irrapx1  41614  scottelrankd  43054  radcnvrat  43121  supminfxr  44222  fsumiunss  44339  dvnprodlem1  44710  stoweidlem15  44779  stoweidlem31  44795  fourierdlem25  44896  fourierdlem51  44921  fourierdlem79  44949  etransclem28  45026  issalgend  45102  sge0iunmptlemre  45179  hoidmvlelem2  45360  issmflem  45491  smfresal  45552  2zrngasgrp  46886  2zrngamnd  46887  2zrngacmnd  46888  2zrngagrp  46889  2zrngmsgrp  46893  2zrngALT  46894  2zrngnmlid  46895  2zrngnmlid2  46897