Theorem elrab 3645

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2402. (Revised by Steven Nguyen, 23-Nov-2022.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		elex 3472	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3472	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2849	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3414	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3413  Vcvv 3451

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453

This theorem is used by:  elrab3  3646  elrabd  3647  elrabrd  3648  elrab2  3649  ralrab  3652  rexrab  3654  reurab  3659  rabsnt  4692  unimax  4905  ssintub  4926  intminss  4934  rabxfrd  5379  ssimaex  6968  weniso  7362  canth  7372  riotarab  7417  sorpsscmpl  7748  onnminsb  7811  dfom2  7877  ssnlim  7895  elsuppfng  8179  elsuppfn  8180  ressuppssdif  8195  oeeulem  8603  cofonr  8676  elpmg  8856  fineqvlem  9250  mapfienlem2  9391  supub  9444  suplub  9445  ordtypelem6  9510  ordtypelem7  9511  hartogslem1  9529  hartogs  9531  wemapsolem  9537  card2on  9541  elharval  9548  wdom2d  9567  cantnfs  9660  scottex  9926  scottexOLD  9927  scottelrankd  9941  tskwe  10024  cardid2  10027  iscard2  10050  cardmin2  10073  acni3  10119  alephsuc2  10152  kmlem1  10222  cofsmo  10340  coftr  10344  fin23lem11  10388  enfin2i  10392  fin1a2lem9  10479  fin1a2lem11  10481  axcc4  10510  axdc3lem2  10522  zorn2lem7  10573  ondomon  10640  alephval2  10650  grutsk  10900  negf1o  11739  infm3  12269  nnind  12346  peano2uz2  12780  peano5uzi  12781  dfuzi  12783  uzind  12784  uzind3  12786  eluz1  12962  uzind4  13026  nnwos  13035  eqreznegel  13054  zmin  13064  elixx1  13478  elioo2  13510  elfz1  13637  flval3  13948  serge0  14192  expge0  14234  expge1  14235  hashbclem  14590  pr2pwpr  14617  elss2prb  14626  hash2sspr  14627  wrdmap  14684  wwlktovfo  15104  shftf  15225  rlimrege0  15739  incexc2  16000  dvdsdivcl  16479  divalglem4  16559  divalgmod  16569  bitsval  16587  bezout  16709  dfgcd2  16712  lcmledvds  16767  lcmgcdlem  16774  lcmfledvds  16800  1nprm  16847  1idssfct  16848  isprm2  16850  hashdvds  16945  phisum  16961  odzval  16962  odzcllem  16963  odzdvds  16966  prmreclem2  17088  prmreclem5  17091  rami  17186  ramub1lem1  17197  ramub1lem2  17198  prmgaplem3  17224  prmgaplem4  17225  prmgaplem5  17226  prmgaplem6  17227  ismre  17753  ismri  17798  isacs  17818  isacs1i  17824  catlid  17850  catrid  17851  ismon  17901  isnat  18118  eldmcoa  18233  fncnvimaeqv  18287  lubeldm  18518  glbeldm  18531  gsumval2  18868  ismgmhm  18878  issubmgm  18884  rabsubmgmd  18886  mgmhmeql  18898  ismhm  18973  issubm  18991  issubmd  18994  mndind  19017  grplinv  19193  issubg  19329  isnsg  19358  cycsubg  19416  isgim  19469  isga  19498  elcntz  19529  elcntzsn  19532  symgfix2  19623  symgsssg  19674  symgfisg  19675  psgnunilem5  19701  odid  19745  odlem2  19746  gexid  19788  gexlem2  19789  gexdvds  19791  isslw  19815  pgpssslw  19821  pj1id  19906  oddvdssubg  20062  pgpfac1lem5  20288  ablfaclem2  20295  isirred  20642  isrnghm  20664  isrngim  20668  isrhm0  20699  isrim0  20706  rimval  20723  issubrng  20792  issubrg  20816  rgspnmin  20860  issdrg  21038  isabv  21061  islss  21202  islmhm  21295  islmim  21330  islbs  21344  isprmidl  21612  psgndiflemB  21899  elocv  21967  isobs  22019  dsmmelbas  22038  frlmelbas  22055  islinds  22108  gsumbagdiaglem  22232  rhmpsrlem2  22242  psrlidm  22262  psrridm  22263  psrass1  22264  psrcom  22268  mplsubglem  22299  mpllsslem  22300  evlsval2  22389  ismhp  22454  ismhp3  22456  mhpmulcl  22463  psdmul  22480  coe1ae0  22527  coe1mul2  22581  dmatel  22801  scmatel  22813  scmateALT  22820  symgmatr01lem  22961  pmatcoe1fsupp  23012  cpmatel  23022  chpscmat  23153  istopon  23223  fctop  23315  cctop  23317  ppttop  23318  pptbas  23319  epttop  23320  iscld  23338  clscld  23358  isnei  23414  neips  23424  neiptopnei  23443  iscn  23546  iscnp  23548  cmpsublem  23710  conncompconn  23743  2ndc1stc  23762  2ndcdisj  23768  elkgen  23848  xkoccn  23931  txdis1cn  23947  txkgen  23964  xkococnlem  23971  xkococn  23972  xkoinjcn  23999  txconn  24001  elqtop  24009  elmptrab  24139  fbssfi  24149  opnfbas  24154  elfg  24183  cfinfil  24205  csdfil  24206  supfil  24207  filssufilg  24223  uffix  24233  fixufil  24234  uffixfr  24235  elflim2  24276  fclscf  24337  flimfnfcls  24340  alexsubALTlem2  24360  alexsubALTlem4  24362  alexsubALT  24363  ptcmplem2  24365  elutop  24545  isucn  24589  iscfilu  24599  ispsmet  24616  ismet  24635  isxmet  24636  elblps  24699  elbl  24700  restmetu  24882  icccmp  25138  elcncf  25203  ishtpy  25286  isphtpy  25295  om1elbas  25346  iscfil  25579  iscau  25590  iscmet  25598  lmle  25615  rrxfsupp  25716  minveclem3  25743  minveclem4  25746  ovolshftlem1  25823  ovolscalem1  25827  ovolicc2lem3  25833  dyadmax  25912  dyadmbllem  25913  opnmbllem  25915  vitalilem2  25923  vitalilem3  25924  elcpn  26247  ig1pval3  26489  coelem  26538  quotlem  26614  elqaalem1  26635  elqaalem3  26637  aannenlem1  26648  aannenlem2  26649  dmarea  27278  jensen  27309  ftalem4  27396  efnnfsumcl  27423  efchtdvds  27479  sqff1o  27502  fsumdvdsdiaglem  27503  dvdsppwf1o  27506  dvdsflf1o  27507  dvdsflsumcom  27508  musum  27511  muinv  27513  logfac2  27537  dchrelbas  27556  lgsfle1  27626  lgsle1  27632  lgsdirprm  27651  lgsne0  27655  lgsquadlem1  27700  lgsquadlem2  27701  dchrvmasumlem1  27815  logsqvma  27862  pntleml  27931  infdesc  27960  ltsval2  28006  ltsres  28012  conway  28158  cutcuts  28160  cutbday  28163  cutsun12  28169  cutbdaybnd2  28175  cutbdaylt  28177  bday1  28193  cutlt  28311  precsexlem8  28593  precsexlem9  28594  precsexlem11  28596  oncutlt  28643  noseqinds  28672  peano5uzs  28783  uzsind  28784  tgellng  29009  mircgr  29122  mirbtwn  29123  elplng  29251  iseqlg  29405  ttgelitv  29453  upgrle  29661  upgrbi  29664  umgredg2  29671  umgrbi  29672  edgupgr  29705  edgumgr  29706  upgredg  29708  numedglnl  29715  edgusgr  29734  usgruspgrb  29757  usgredg2ALT  29767  ushgredgedg  29803  ushgredgedgloop  29805  usgrexmplef  29833  upgrreslem  29878  umgrreslem  29879  upgrres1  29887  nbgrel  29914  nbupgrel  29919  nbumgrvtx  29920  nbusgreledg  29927  nbgrnself  29933  uvtxusgrel  29977  vtxdgoddnumeven  30127  rgrusgrprc  30163  lfgrwlkprop  30263  iswwlks  30418  iswwlksn  30420  wwlksnextsurj  30482  rusgrnumwwlkslem  30554  rusgrnumwwlks  30559  isclwwlk  30568  clwwlknscsh  30646  eleclclwwlkn  30660  clwlknf1oclwwlkn  30668  clwwlkvbij  30697  eupth2lems  30832  konigsberglem4  30849  fusgreg2wsplem  30927  2clwwlkel  30943  extwwlkfabel  30947  clwwlknonclwlknonf1o  30956  dlwwlknondlwlknonf1o  30959  numclwwlk2lem1  30970  numclwlk2lem2f  30971  numclwlk2lem2f1o  30973  grpoidinv2  31110  grpoinv  31120  isssp  31319  islno  31348  isblo  31377  ishmo  31406  ubthlem1  31465  ubthlem2  31466  htthlem  31512  ocel  31876  shsval2i  31982  ococin  32003  chsupsn  32008  eleigvec  32552  cnlnadjlem5  32666  shatomistici  32956  hatomistici  32957  dmrab  33086  nnindf  33404  indf1ofs  33426  ismnt  33537  pwrssmgc  33554  tocycf  33671  tocyc01  33672  trsp2cyc  33677  cycpmco2f1  33678  cycpmco2rn  33679  cycpmco2lem2  33681  cycpmco2lem3  33682  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2lem7  33686  cycpmconjv  33696  tocyccntz  33698  cyc3evpm  33704  cycpmgcl  33707  cyc3conja  33711  isfxp  33722  fxpgaeq  33723  elrgspnsubrun  33803  rlocisunit  33830  fldgensdrg  33869  nsgmgclem  33955  nsgmgc  33956  nsgqusf1olem2  33958  ismxidl  33980  ssmxidl  33992  isrprm  34042  1arithufdlem3  34071  1arithufdlem4  34072  1arithufd  34073  mplvrpmga  34170  mplvrpmmhm  34171  fedgmullem2  34255  ply1annnr  34328  minplyann  34334  minplyirred  34336  constrsuc  34363  zarclsiin  34496  zart0  34504  rhmpreimacnlem  34509  ordtconnlem1  34549  sigagenval  34766  ldsysgenld  34786  ldgenpisyslem1  34789  ldgenpisyslem2  34790  ldgenpisys  34792  ddemeas  34862  ismbfm  34877  imambfm  34887  dya2iocuni  34908  oms0  34922  omssubadd  34925  elcarsg  34930  issibf  34958  sitgfval  34966  oddpwdc  34979  eulerpartlemgh  35003  eulerpartlemgs2  35005  dstfrvel  35099  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemiex  35127  ballotlemfrcn0  35155  ballotlemirc  35157  ballotlem7  35161  reprsum  35235  reprsuc  35237  reprpmtf1o  35248  reprdifc  35249  fnrelpredd  35709  fineqvnttrclselem2  35773  connpconn  35979  iscvm  36003  cvmsi  36009  cvmsval  36010  cvmliftmolem2  36026  cvmliftiota  36045  snmlval  36075  satfv1lem  36106  fmlafvel  36129  fmla1  36131  fmlaomn0  36134  satfv0fvfmla0  36157  sategoelfvb  36163  elmpst  36280  lineelsb2  36893  linerflx1  36894  fwddifval  36907  fwddifnval  36908  rankeq1o  36912  finminlem  37086  fneint  37116  fnessref  37125  topmeet  37132  topjoin  37133  neifg  37139  weiunlem  37231  weiunfrlem  37232  weiunse  37236  regsfromregtco  37306  relowlssretop  38266  fin2solem  38509  fin2so  38510  poimirlem4  38522  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  poimirlem32  38550  opnmbllem0  38554  mblfinlem2  38556  itg2gt0cn  38573  indexa  38647  nninfnub  38665  istotbnd  38683  sstotbnd2  38688  isbnd  38694  isrngohom  38879  isrngoiso  38892  isidl  38928  ispridl  38948  ismaxidl  38954  prnc  38981  isfldidl  38982  islshp  40016  lssats  40049  islfl  40097  isat  40323  atlatmstc  40356  islln  40543  islpln  40567  islvol  40610  linepsubN  40789  elpmap  40795  pmapsub  40805  elpadd  40836  paddvaln0N  40838  islhp  41033  isldil  41147  isltrn  41156  isdilN  41191  istrnN  41194  diaval  42069  diaelval  42070  diaeldm  42073  diaelrnN  42082  cdlemm10N  42155  docaclN  42161  dibglbN  42203  dicval  42213  dicfnN  42220  dicvalrelN  42222  dihglblem2aN  42330  dihglblem2N  42331  dihglblem3N  42332  dih1dimatlem  42366  dihglb2  42379  dochvalr  42394  doch2val2  42401  dochocss  42403  islpolN  42520  mapd0  42702  aks4d1p4  43109  aks4d1p7  43113  isprimroot  43123  linvh  43126  primrootsunit1  43127  primrootscoprmpow  43129  primrootscoprbij  43132  sticksstones3  43178  aks6d1c6lem3  43202  grpods  43224  unitscyglem2  43226  unitscyglem4  43228  unitscyglem5  43229  supinf  43273  fsuppssindlem2  43600  isnacs  43694  elmzpcl  43716  mzpindd  43736  rencldnfilem  43806  irrapxlem6  43813  pellexlem3  43817  pellexlem5  43819  elpell1qr  43833  elpell14qr  43835  elpell1234qr  43837  pellfundre  43867  pellfundge  43868  pellfundlb  43870  pellfundglb  43871  rmspecnonsq  43893  jm2.22  43981  jm2.23  43982  rpnnen3lem  44017  fnwe2lem2  44037  elmnc  44122  dgraalem  44131  dgraaub  44134  mpaalem  44138  onsucelab  44249  limnsuc  44251  sqrtcvallem1  44616  rfovcnvf1od  44989  nzss  45286  iccshift  46499  iooshift  46503  limcperiod  46609  sumnnodd  46611  ioodvbdlimc1lem1  46910  dvnprodlem1  46925  dvnprodlem3  46927  itgperiod  46960  stoweidlem14  46993  stoweidlem15  46994  stoweidlem16  46995  stoweidlem31  47010  stoweidlem36  47015  stoweidlem46  47025  stoweidlem48  47027  fourierdlem2  47088  fourierdlem3  47089  fourierdlem20  47106  fourierdlem25  47111  fourierdlem37  47123  fourierdlem42  47128  fourierdlem48  47133  fourierdlem51  47136  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem79  47164  fourierdlem81  47166  elaa2lem  47212  etransclem24  47237  etransclem26  47239  etransclem28  47241  etransclem35  47248  etransclem48  47261  salgenval  47300  salgenn0  47310  salgencl  47311  sssalgen  47314  salgenss  47315  salgenuni  47316  issalgend  47317  salgencntex  47322  subsaliuncllem  47336  sge0fodjrnlem  47395  meadjiunlem  47444  caragenel  47474  ovnlecvr  47537  ovnpnfelsup  47538  ovncvrrp  47543  ovnsubaddlem1  47549  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem4  47577  ovnhoilem1  47580  ovnlecvr2  47589  ovncvr2  47590  issmflem  47706  smflimlem2  47751  smflimlem3  47752  smflimsuplem2  47800  elsetpreimafvrab  48445  iccpart  48467  sprel  48535  prelspr  48537  sprsymrelfolem2  48544  sprsymrelf  48546  prpair  48552  paireqne  48562  prprelb  48567  prprelprb  48568  dfodd2  48703  dfeven5  48733  dfodd7  48734  fpprel  48795  clnbgrel  48895  clnbupgrel  48901  sclnbgrel  48914  vopnbgrel  48921  dfclnbgr6  48923  dfnbgr6  48924  isubgredg  48933  uhgrimisgrgric  48998  grtriprop  49008  isgrtri  49010  stgredgel  49024  stgrusgra  49026  uspgrlimlem3  49057  uspgrlim  49059  grlimgredgex  49067  grlimgrtrilem2  49069  gpgiedgdmel  49116  gpgedgel  49117  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  gpgprismgr4cycllem10  49171  1hegrlfgr  49199  assintop  49275  isassintop  49276  assintopcllaw  49278  0even  49303  2even  49305  2zrngamgm  49311  dmatALTbasel  49483  lcoval  49493  elbigo  49632  elrrx2linest2  49826  itsclc0  49852  itsclc0b  49853  itscnhlinecirc02p  49866  unilbss  49897  secval  50809  cscval  50810  cotval  50811  dvsec  50825  dvcsc  50826  dvcot  50827