Theorem elrabi 3655

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 2182, ax-11 2198, ax-12 2219. (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 2845	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2748	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 487	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2114	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2896	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 221	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 220	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2857	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 481	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 604	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1957	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 220	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3424	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2887	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ∃wex 1806  [wsb 2097   ∈ wcel 2149  {cab 2747  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  ssrab2  4042  elfvmptrab1w  7018  elfvmptrab1  7019  elovmporab  7657  elovmporab1w  7658  elovmporab1  7659  elovmpt3rab1  7671  mapfienlem1  9365  mapfienlem2  9366  mapfienlem3  9367  scottelrankd  9873  kmlem1  10134  fin1a2lem9  10392  ac6num  10463  nnind  12251  ublbneg  12957  supminf  12959  rlimrege0  15630  incexc2  15892  lcmgcdlem  16664  phisum  16850  prmgaplem5  17115  isinitoi  18056  istermoi  18057  odcl  19606  odlem2  19609  gexcl  19650  gexlem2  19652  gexdvds  19654  pgpssslw  19684  psgnfix2  21718  psgndiflemB  21719  psgndif  21721  copsgndif  21722  psrbagf  22037  psrbagleadd1  22047  resspsrmul  22094  mplbas2  22162  rhmcomulmpl  22244  mhpmulcl  22281  psdmul  22298  mptcoe1fsupp  22344  psropprmul  22366  coe1mul2  22399  cpmatpmat  22836  mptcoe1matfsupp  22928  mp2pm2mplem4  22935  chpscmat  22968  chpscmatgsumbin  22970  chpscmatgsummon  22971  txdis1cn  23761  ptcmplem3  24180  rrxmvallem  25532  mdegmullem  26204  0sgm  27274  sgmf  27275  sgmnncl  27277  fsumdvdsdiaglem  27313  fsumdvdscom  27315  dvdsppwf1o  27316  dvdsflf1o  27317  musumsum  27322  muinv  27323  sgmppw  27327  rpvmasumlem  27617  dchrmusum2  27624  dchrvmasumlem1  27625  dchrvmasum2lem  27626  dchrisum0fmul  27636  dchrisum0ff  27637  dchrisum0flblem1  27638  dchrisum0  27650  logsqvma  27672  precsexlem9  28374  usgredg2v  29518  umgrres1lem  29601  upgrres1  29604  vtxdgoddnumeven  29844  rusgrnumwwlks  30267  frgrwopreglem4  30607  frgrwopreg  30615  rabsnel  32787  nnindf  33105  cyc3evpm  33411  cycpmgcl  33414  cycpmconjslem2  33416  elrgspnsubrun  33510  nsgmgclem  33664  mplvrpmrhm  33882  ddemeas  34571  imambfm  34597  eulerpartlemgs2  34715  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemirc  34867  reprf  34944  tgoldbachgnn  34991  tgoldbachgt  34995  bnj110  35191  fnrelpredd  35425  wevgblacfn  35528  weiunlem  36897  poimirlem4  38197  poimirlem5  38198  poimirlem6  38199  poimirlem7  38200  poimirlem8  38201  poimirlem9  38202  poimirlem10  38203  poimirlem11  38204  poimirlem12  38205  poimirlem13  38206  poimirlem14  38207  poimirlem15  38208  poimirlem16  38209  poimirlem17  38210  poimirlem18  38211  poimirlem19  38212  poimirlem20  38213  poimirlem21  38214  poimirlem22  38215  poimirlem26  38219  mblfinlem2  38231  primrootsunit1  42788  hashscontpow1  42812  aks6d1c6lem2  42862  aks6d1c6lem3  42863  grpods  42885  rhmcomulpsr  43240  mhphflem  43254  mhphf  43255  rencldnfilem  43473  irrapx1  43481  radcnvrat  44950  supminfxr  46104  fsumiunss  46217  dvnprodlem1  46586  stoweidlem15  46655  stoweidlem31  46671  fourierdlem25  46772  fourierdlem51  46797  fourierdlem79  46825  etransclem28  46902  issalgend  46978  sge0iunmptlemre  47055  hoidmvlelem2  47236  issmflem  47367  smfresal  47428  2zrngasgrp  48934  2zrngamnd  48935  2zrngacmnd  48936  2zrngagrp  48937  2zrngmsgrp  48941  2zrngALT  48942  2zrngnmlid  48943  2zrngnmlid2  48945