Theorem elrabi 3618

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 2137, ax-11 2154, ax-12 2171. (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 2817	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2716	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 483	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2077	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2866	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 217	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 216	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 477	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1933	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 216	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3073	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2857	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ∃wex 1782  [wsb 2067   ∈ wcel 2106  {cab 2715  {crab 3068

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073

This theorem is referenced by:  ssrab2  4013  elfvmptrab1w  6901  elfvmptrab1  6902  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  elovmpt3rab1  7529  mapfienlem1  9164  mapfienlem2  9165  mapfienlem3  9166  kmlem1  9906  fin1a2lem9  10164  ac6num  10235  nnind  11991  ublbneg  12673  supminf  12675  rlimrege0  15288  incexc2  15550  lcmgcdlem  16311  phisum  16491  prmgaplem5  16756  isinitoi  17714  istermoi  17715  odcl  19144  odlem2  19147  gexcl  19185  gexlem2  19187  gexdvds  19189  pgpssslw  19219  psgnfix2  20804  psgndiflemB  20805  psgndif  20807  copsgndif  20808  psrbagf  21121  resspsrmul  21186  mplbas2  21243  mhpmulcl  21339  mptcoe1fsupp  21386  psropprmul  21409  coe1mul2  21440  cpmatpmat  21859  mptcoe1matfsupp  21951  mp2pm2mplem4  21958  chpscmat  21991  chpscmatgsumbin  21993  chpscmatgsummon  21994  txdis1cn  22786  ptcmplem3  23205  rrxmvallem  24568  mdegmullem  25243  0sgm  26293  sgmf  26294  sgmnncl  26296  fsumdvdsdiaglem  26332  fsumdvdscom  26334  dvdsppwf1o  26335  dvdsflf1o  26336  musumsum  26341  muinv  26342  sgmppw  26345  rpvmasumlem  26635  dchrmusum2  26642  dchrvmasumlem1  26643  dchrvmasum2lem  26644  dchrisum0fmul  26654  dchrisum0ff  26655  dchrisum0flblem1  26656  dchrisum0  26668  logsqvma  26690  usgredg2v  27594  umgrres1lem  27677  upgrres1  27680  vtxdgoddnumeven  27920  rusgrnumwwlks  28339  frgrwopreglem4  28679  frgrwopreg  28687  rabsnel  30847  nnindf  31133  cyc3evpm  31417  cycpmgcl  31420  cycpmconjslem2  31422  nsgmgclem  31596  ddemeas  32204  imambfm  32229  eulerpartlemgs2  32347  ballotlemfc0  32459  ballotlemfcc  32460  ballotlemirc  32498  reprf  32592  tgoldbachgnn  32639  tgoldbachgt  32643  bnj110  32838  fnrelpredd  33061  poimirlem4  35781  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem9  35786  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem26  35803  mblfinlem2  35815  mhphflem  40284  mhphf  40285  rencldnfilem  40642  irrapx1  40650  scottelrankd  41865  radcnvrat  41932  supminfxr  43004  fsumiunss  43116  dvnprodlem1  43487  stoweidlem15  43556  stoweidlem31  43572  fourierdlem25  43673  fourierdlem51  43698  fourierdlem79  43726  etransclem28  43803  issalgend  43877  sge0iunmptlemre  43953  hoidmvlelem2  44134  issmflem  44263  smfresal  44322  2zrngasgrp  45498  2zrngamnd  45499  2zrngacmnd  45500  2zrngagrp  45501  2zrngmsgrp  45505  2zrngALT  45506  2zrngnmlid  45507  2zrngnmlid2  45509