Theorem elrabi 3656

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 2142, ax-11 2158, ax-12 2178. (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 2805	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}))
2		df-clab 2709	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} ↔ [𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑))
3		simpl 482	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑥 ∈ 𝑉)
4	3	sbimi 2075	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → [𝑦 / 𝑥]𝑥 ∈ 𝑉)
5		clelsb1 2856	. . . . . . 7 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑉 ↔ 𝑦 ∈ 𝑉)
6	4, 5	sylib 218	. . . . . 6 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑉 ∧ 𝜑) → 𝑦 ∈ 𝑉)
7	2, 6	sylbi 217	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝑦 ∈ 𝑉)
8		eleq1 2817	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉))
9	8	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → 𝐴 ∈ 𝑉)
10	7, 9	sylan2 593	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
11	10	exlimiv 1930	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}) → 𝐴 ∈ 𝑉)
12	1, 11	sylbi 217	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)} → 𝐴 ∈ 𝑉)
13		df-rab 3409	. 2 ⊢ {𝑥 ∈ 𝑉 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝑉 ∧ 𝜑)}
14	12, 13	eleq2s 2847	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝑉 ∣ 𝜑} → 𝐴 ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2708  {crab 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  ssrab2  4045  elfvmptrab1w  6997  elfvmptrab1  6998  elovmporab  7637  elovmporab1w  7638  elovmporab1  7639  elovmpt3rab1  7651  mapfienlem1  9362  mapfienlem2  9363  mapfienlem3  9364  kmlem1  10110  fin1a2lem9  10367  ac6num  10438  nnind  12205  ublbneg  12898  supminf  12900  rlimrege0  15551  incexc2  15810  lcmgcdlem  16582  phisum  16767  prmgaplem5  17032  isinitoi  17967  istermoi  17968  odcl  19472  odlem2  19475  gexcl  19516  gexlem2  19518  gexdvds  19520  pgpssslw  19550  psgnfix2  21514  psgndiflemB  21515  psgndif  21517  copsgndif  21518  psrbagf  21833  psrbagleadd1  21843  resspsrmul  21891  mplbas2  21955  mhpmulcl  22042  psdmul  22059  mptcoe1fsupp  22106  psropprmul  22128  coe1mul2  22161  rhmcomulmpl  22275  cpmatpmat  22603  mptcoe1matfsupp  22695  mp2pm2mplem4  22702  chpscmat  22735  chpscmatgsumbin  22737  chpscmatgsummon  22738  txdis1cn  23528  ptcmplem3  23947  rrxmvallem  25310  mdegmullem  25989  0sgm  27060  sgmf  27061  sgmnncl  27063  fsumdvdsdiaglem  27099  fsumdvdscom  27101  dvdsppwf1o  27102  dvdsflf1o  27103  musumsum  27108  muinv  27109  sgmppw  27114  rpvmasumlem  27404  dchrmusum2  27411  dchrvmasumlem1  27412  dchrvmasum2lem  27413  dchrisum0fmul  27423  dchrisum0ff  27424  dchrisum0flblem1  27425  dchrisum0  27437  logsqvma  27459  precsexlem9  28123  usgredg2v  29160  umgrres1lem  29243  upgrres1  29246  vtxdgoddnumeven  29487  rusgrnumwwlks  29910  frgrwopreglem4  30250  frgrwopreg  30258  rabsnel  32435  nnindf  32750  cyc3evpm  33113  cycpmgcl  33116  cycpmconjslem2  33118  elrgspnsubrun  33206  nsgmgclem  33388  ddemeas  34232  imambfm  34259  eulerpartlemgs2  34377  ballotlemfc0  34490  ballotlemfcc  34491  ballotlemirc  34529  reprf  34609  tgoldbachgnn  34656  tgoldbachgt  34660  bnj110  34854  fnrelpredd  35085  wevgblacfn  35096  weiunlem2  36446  poimirlem4  37613  poimirlem5  37614  poimirlem6  37615  poimirlem7  37616  poimirlem8  37617  poimirlem9  37618  poimirlem10  37619  poimirlem11  37620  poimirlem12  37621  poimirlem13  37622  poimirlem14  37623  poimirlem15  37624  poimirlem16  37625  poimirlem17  37626  poimirlem18  37627  poimirlem19  37628  poimirlem20  37629  poimirlem21  37630  poimirlem22  37631  poimirlem26  37635  mblfinlem2  37647  primrootsunit1  42080  hashscontpow1  42104  aks6d1c6lem2  42154  aks6d1c6lem3  42155  grpods  42177  rhmcomulpsr  42532  mhphflem  42577  mhphf  42578  rencldnfilem  42801  irrapx1  42809  scottelrankd  44229  radcnvrat  44296  supminfxr  45453  fsumiunss  45566  dvnprodlem1  45937  stoweidlem15  46006  stoweidlem31  46022  fourierdlem25  46123  fourierdlem51  46148  fourierdlem79  46176  etransclem28  46253  issalgend  46329  sge0iunmptlemre  46406  hoidmvlelem2  46587  issmflem  46718  smfresal  46779  2zrngasgrp  48224  2zrngamnd  48225  2zrngacmnd  48226  2zrngagrp  48227  2zrngmsgrp  48231  2zrngALT  48232  2zrngnmlid  48233  2zrngnmlid2  48235