Theorem elrab 3676

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2375. (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 3485	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3485	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2821	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3421	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3664	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {crab 3420  Vcvv 3464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466

This theorem is referenced by:  elrab3  3677  elrabd  3678  elrab2  3679  ralrab  3683  rexrab  3686  reurab  3691  rabsnt  4713  unimax  4926  ssintub  4948  intminss  4956  rabxfrd  5399  ssimaex  6975  weniso  7357  canth  7368  riotarab  7413  sorpsscmpl  7737  onnminsb  7802  dfom2  7872  ssnlim  7890  elsuppfng  8177  elsuppfn  8178  ressuppssdif  8193  oeeulem  8622  cofonr  8695  elpmg  8866  fineqvlem  9281  mapfienlem2  9429  supub  9482  suplub  9483  ordtypelem6  9546  ordtypelem7  9547  hartogslem1  9565  hartogs  9567  wemapsolem  9573  card2on  9577  elharval  9584  wdom2d  9603  cantnfs  9689  scottex  9908  tskwe  9973  cardid2  9976  iscard2  9999  cardmin2  10022  acni3  10070  alephsuc2  10103  kmlem1  10174  cofsmo  10292  coftr  10296  fin23lem11  10340  enfin2i  10344  fin1a2lem9  10431  fin1a2lem11  10433  axcc4  10462  axdc3lem2  10474  zorn2lem7  10525  ondomon  10586  alephval2  10595  grutsk  10845  negf1o  11676  infm3  12210  nnind  12267  peano2uz2  12690  peano5uzi  12691  dfuzi  12693  uzind  12694  uzind3  12696  eluz1  12865  uzind4  12931  nnwos  12940  eqreznegel  12959  zmin  12969  elixx1  13379  elioo2  13411  elfz1  13535  flval3  13838  serge0  14080  expge0  14122  expge1  14123  hashbclem  14474  pr2pwpr  14501  elss2prb  14510  hash2sspr  14511  wrdmap  14567  wwlktovfo  14980  shftf  15101  rlimrege0  15598  incexc2  15857  dvdsdivcl  16336  divalglem4  16416  divalgmod  16426  bitsval  16444  bezout  16563  dfgcd2  16566  lcmledvds  16619  lcmgcdlem  16626  lcmfledvds  16652  1nprm  16699  1idssfct  16700  isprm2  16702  hashdvds  16795  phisum  16811  odzval  16812  odzcllem  16813  odzdvds  16816  prmreclem2  16938  prmreclem5  16941  rami  17036  ramub1lem1  17047  ramub1lem2  17048  prmgaplem3  17074  prmgaplem4  17075  prmgaplem5  17076  prmgaplem6  17077  ismre  17609  ismri  17650  isacs  17670  isacs1i  17676  catlid  17702  catrid  17703  ismon  17753  isnat  17971  eldmcoa  18086  fncnvimaeqv  18140  lubeldm  18372  glbeldm  18385  gsumval2  18673  ismgmhm  18683  issubmgm  18689  rabsubmgmd  18691  mgmhmeql  18703  ismhm  18772  issubm  18790  issubmd  18793  mndind  18815  grplinv  18981  issubg  19118  isnsg  19147  cycsubg  19200  isgim  19254  isga  19283  elcntz  19314  elcntzsn  19317  symgfix2  19407  symgsssg  19458  symgfisg  19459  psgnunilem5  19485  odid  19529  odlem2  19530  gexid  19572  gexlem2  19573  gexdvds  19575  isslw  19599  pgpssslw  19605  pj1id  19690  oddvdssubg  19846  pgpfac1lem5  20072  ablfaclem2  20079  isirred  20392  isrnghm  20414  isrngim  20418  isrim0OLD  20454  isrim0  20456  issubrng  20520  issubrg  20544  rgspnmin  20588  issdrg  20762  isabv  20785  islss  20905  islmhm  20999  islmim  21034  islbs  21048  psgndiflemB  21585  elocv  21653  isobs  21707  dsmmelbas  21726  frlmelbas  21743  islinds  21796  gsumbagdiaglem  21917  rhmpsrlem2  21928  psrlidm  21949  psrridm  21950  psrass1  21951  psrcom  21955  mplsubglem  21986  mpllsslem  21987  evlsval2  22078  ismhp  22111  ismhp3  22113  mhpmulcl  22120  psdmul  22137  coe1ae0  22185  coe1mul2  22239  dmatel  22466  scmatel  22478  scmateALT  22485  symgmatr01lem  22626  pmatcoe1fsupp  22674  cpmatel  22684  chpscmat  22815  istopon  22885  fctop  22977  cctop  22979  ppttop  22980  pptbas  22981  epttop  22982  iscld  23000  clscld  23020  isnei  23076  neips  23086  neiptopnei  23105  iscn  23208  iscnp  23210  cmpsublem  23372  conncompconn  23405  2ndc1stc  23424  2ndcdisj  23429  elkgen  23509  xkoccn  23592  txdis1cn  23608  txkgen  23625  xkococnlem  23632  xkococn  23633  xkoinjcn  23660  txconn  23662  elqtop  23670  elmptrab  23800  fbssfi  23810  opnfbas  23815  elfg  23844  cfinfil  23866  csdfil  23867  supfil  23868  filssufilg  23884  uffix  23894  fixufil  23895  uffixfr  23896  elflim2  23937  fclscf  23998  flimfnfcls  24001  alexsubALTlem2  24021  alexsubALTlem4  24023  alexsubALT  24024  ptcmplem2  24026  elutop  24207  isucn  24251  iscfilu  24261  ispsmet  24278  ismet  24297  isxmet  24298  elblps  24361  elbl  24362  restmetu  24546  icccmp  24802  elcncf  24870  ishtpy  24959  isphtpy  24968  om1elbas  25020  iscfil  25254  iscau  25265  iscmet  25273  lmle  25290  rrxfsupp  25391  minveclem3  25418  minveclem4  25421  ovolshftlem1  25499  ovolscalem1  25503  ovolicc2lem3  25509  dyadmax  25588  dyadmbllem  25589  opnmbllem  25591  vitalilem2  25599  vitalilem3  25600  elcpn  25925  ig1pval3  26172  coelem  26220  quotlem  26297  elqaalem1  26316  elqaalem3  26318  aannenlem1  26325  aannenlem2  26326  dmarea  26955  jensen  26987  ftalem4  27074  efnnfsumcl  27101  efchtdvds  27157  sqff1o  27180  fsumdvdsdiaglem  27181  dvdsppwf1o  27184  dvdsflf1o  27185  dvdsflsumcom  27186  musum  27189  muinv  27191  logfac2  27216  dchrelbas  27235  lgsfle1  27305  lgsle1  27311  lgsdirprm  27330  lgsne0  27334  lgsquadlem1  27379  lgsquadlem2  27380  dchrvmasumlem1  27494  logsqvma  27541  pntleml  27610  sltval2  27656  sltres  27662  conway  27799  scutcut  27801  scutbday  27804  scutun12  27810  scutbdaybnd2  27816  scutbdaylt  27818  bday1s  27831  cutlt  27921  precsexlem8  28193  precsexlem9  28194  precsexlem11  28196  noseqinds  28254  peano5uzs  28345  uzsind  28346  tgellng  28516  mircgr  28620  mirbtwn  28621  iseqlg  28830  ttgelitv  28847  upgrle  29054  upgrbi  29057  umgredg2  29064  umgrbi  29065  edgupgr  29098  edgumgr  29099  upgredg  29101  numedglnl  29108  edgusgr  29124  usgruspgrb  29147  usgredg2ALT  29157  ushgredgedg  29193  ushgredgedgloop  29195  usgrexmplef  29223  upgrreslem  29268  umgrreslem  29269  upgrres1  29277  nbgrel  29304  nbupgrel  29309  nbumgrvtx  29310  nbusgreledg  29317  nbgrnself  29323  uvtxusgrel  29367  vtxdgoddnumeven  29518  rgrusgrprc  29554  lfgrwlkprop  29652  iswwlks  29803  iswwlksn  29805  wwlksnextsurj  29867  rusgrnumwwlkslem  29936  rusgrnumwwlks  29941  isclwwlk  29950  clwwlknscsh  30028  eleclclwwlkn  30042  clwlknf1oclwwlkn  30050  clwwlkvbij  30079  eupth2lems  30204  konigsberglem4  30221  fusgreg2wsplem  30299  2clwwlkel  30315  extwwlkfabel  30319  clwwlknonclwlknonf1o  30328  dlwwlknondlwlknonf1o  30331  numclwwlk2lem1  30342  numclwlk2lem2f  30343  numclwlk2lem2f1o  30345  grpoidinv2  30481  grpoinv  30491  isssp  30690  islno  30719  isblo  30748  ishmo  30777  ubthlem1  30836  ubthlem2  30837  htthlem  30883  ocel  31247  shsval2i  31353  ococin  31374  chsupsn  31379  eleigvec  31923  cnlnadjlem5  32037  shatomistici  32327  hatomistici  32328  dmrab  32463  nnindf  32768  indf1ofs  32798  ismnt  32919  pwrssmgc  32936  tocycf  33083  tocyc01  33084  trsp2cyc  33089  cycpmco2f1  33090  cycpmco2rn  33091  cycpmco2lem2  33093  cycpmco2lem3  33094  cycpmco2lem5  33096  cycpmco2lem6  33097  cycpmco2lem7  33098  cycpmconjv  33108  tocyccntz  33110  cyc3evpm  33116  cycpmgcl  33119  cycpmconjslem2  33121  cyc3conja  33123  elrgspnsubrun  33199  fldgensdrg  33262  nsgmgclem  33380  nsgmgc  33381  nsgqusf1olem2  33383  isprmidl  33407  ismxidl  33431  ssmxidl  33443  isrprm  33486  1arithufdlem3  33515  1arithufdlem4  33516  1arithufd  33517  fedgmullem2  33622  ply1annnr  33687  minplyann  33693  minplyirred  33695  constrsuc  33720  zarclsiin  33811  zart0  33819  rhmpreimacnlem  33824  ordtconnlem1  33864  sigagenval  34082  ldsysgenld  34102  ldgenpisyslem1  34105  ldgenpisyslem2  34106  ldgenpisys  34108  ddemeas  34178  ismbfm  34193  imambfm  34205  dya2iocuni  34226  oms0  34240  omssubadd  34243  elcarsg  34248  issibf  34276  sitgfval  34284  oddpwdc  34297  eulerpartlemgh  34321  eulerpartlemgs2  34323  dstfrvel  34417  ballotlemfc0  34436  ballotlemfcc  34437  ballotlemiex  34445  ballotlemfrcn0  34473  ballotlemirc  34475  ballotlem7  34479  reprsum  34569  reprsuc  34571  reprpmtf1o  34582  reprdifc  34583  fnrelpredd  35044  connpconn  35181  iscvm  35205  cvmsi  35211  cvmsval  35212  cvmliftmolem2  35228  cvmliftiota  35247  snmlval  35277  satfv1lem  35308  fmlafvel  35331  fmla1  35333  fmlaomn0  35336  satfv0fvfmla0  35359  sategoelfvb  35365  elmpst  35482  lineelsb2  36090  linerflx1  36091  fwddifval  36104  fwddifnval  36105  rankeq1o  36113  finminlem  36260  fneint  36290  fnessref  36299  topmeet  36306  topjoin  36307  neifg  36313  weiunlem2  36405  weiunfrlem  36406  weiunse  36410  relowlssretop  37305  fin2solem  37554  fin2so  37555  poimirlem4  37572  poimirlem25  37593  poimirlem26  37594  poimirlem27  37595  poimirlem31  37599  poimirlem32  37600  opnmbllem0  37604  mblfinlem2  37606  itg2gt0cn  37623  indexa  37681  nninfnub  37699  istotbnd  37717  sstotbnd2  37722  isbnd  37728  isrngohom  37913  isrngoiso  37926  isidl  37962  ispridl  37982  ismaxidl  37988  prnc  38015  isfldidl  38016  islshp  38921  lssats  38954  islfl  39002  isat  39228  atlatmstc  39261  islln  39449  islpln  39473  islvol  39516  linepsubN  39695  elpmap  39701  pmapsub  39711  elpadd  39742  paddvaln0N  39744  islhp  39939  isldil  40053  isltrn  40062  isdilN  40097  istrnN  40100  diaval  40975  diaelval  40976  diaeldm  40979  diaelrnN  40988  cdlemm10N  41061  docaclN  41067  dibglbN  41109  dicval  41119  dicfnN  41126  dicvalrelN  41128  dihglblem2aN  41236  dihglblem2N  41237  dihglblem3N  41238  dih1dimatlem  41272  dihglb2  41285  dochvalr  41300  doch2val2  41307  dochocss  41309  islpolN  41426  mapd0  41608  aks4d1p4  42021  aks4d1p7  42025  isprimroot  42035  linvh  42038  primrootsunit1  42039  primrootscoprmpow  42041  primrootscoprbij  42044  sticksstones3  42090  aks6d1c6lem3  42114  grpods  42136  unitscyglem2  42138  unitscyglem4  42140  unitscyglem5  42141  supinf  42223  fsuppssindlem2  42547  infdesc  42598  isnacs  42660  elmzpcl  42682  mzpindd  42702  rencldnfilem  42776  irrapxlem6  42783  pellexlem3  42787  pellexlem5  42789  elpell1qr  42803  elpell14qr  42805  elpell1234qr  42807  pellfundre  42837  pellfundge  42838  pellfundlb  42840  pellfundglb  42841  rmspecnonsq  42863  jm2.22  42952  jm2.23  42953  rpnnen3lem  42988  fnwe2lem2  43008  elmnc  43093  dgraalem  43102  dgraaub  43105  mpaalem  43109  onsucelab  43221  limnsuc  43223  sqrtcvallem1  43589  rfovcnvf1od  43962  scottelrankd  44211  nzss  44281  iccshift  45476  iooshift  45480  limcperiod  45588  sumnnodd  45590  ioodvbdlimc1lem1  45891  dvnprodlem1  45906  dvnprodlem3  45908  itgperiod  45941  stoweidlem14  45974  stoweidlem15  45975  stoweidlem16  45976  stoweidlem31  45991  stoweidlem36  45996  stoweidlem46  46006  stoweidlem48  46008  fourierdlem2  46069  fourierdlem3  46070  fourierdlem20  46087  fourierdlem25  46092  fourierdlem37  46104  fourierdlem42  46109  fourierdlem48  46114  fourierdlem51  46117  fourierdlem63  46129  fourierdlem64  46130  fourierdlem65  46131  fourierdlem79  46145  fourierdlem81  46147  elaa2lem  46193  etransclem24  46218  etransclem26  46220  etransclem28  46222  etransclem35  46229  etransclem48  46242  salgenval  46281  salgenn0  46291  salgencl  46292  sssalgen  46295  salgenss  46296  salgenuni  46297  issalgend  46298  salgencntex  46303  subsaliuncllem  46317  sge0fodjrnlem  46376  meadjiunlem  46425  caragenel  46455  ovnlecvr  46518  ovnpnfelsup  46519  ovncvrrp  46524  ovnsubaddlem1  46530  hoidmv1lelem1  46551  hoidmv1lelem2  46552  hoidmv1lelem3  46553  hoidmvlelem1  46555  hoidmvlelem2  46556  hoidmvlelem4  46558  ovnhoilem1  46561  ovnlecvr2  46570  ovncvr2  46571  issmflem  46687  smflimlem2  46732  smflimlem3  46733  smflimsuplem2  46781  elsetpreimafvrab  47327  iccpart  47349  sprel  47417  prelspr  47419  sprsymrelfolem2  47426  sprsymrelf  47428  prpair  47434  paireqne  47444  prprelb  47449  prprelprb  47450  dfodd2  47569  dfeven5  47599  dfodd7  47600  fpprel  47661  clnbgrel  47761  clnbupgrel  47767  sclnbgrel  47779  vopnbgrel  47786  dfclnbgr6  47788  dfnbgr6  47789  isubgredg  47798  uhgrimisgrgric  47845  grtriprop  47854  isgrtri  47856  stgredgel  47870  stgrusgra  47872  uspgrlimlem3  47903  uspgrlim  47905  grlimgrtrilem1  47907  grlimgrtrilem2  47908  gpgedgel  47953  gpgnbgrvtx0  47976  gpgnbgrvtx1  47977  1hegrlfgr  47994  assintop  48071  isassintop  48072  assintopcllaw  48074  0even  48099  2even  48101  2zrngamgm  48107  dmatALTbasel  48265  lcoval  48275  elbigo  48418  elrrx2linest2  48612  itsclc0  48638  itsclc0b  48639  itscnhlinecirc02p  48652  unilbss  48683  secval  49262  cscval  49263  cotval  49264