Theorem elrab 3652

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2406. (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 3478	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3478	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 486	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2853	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 644	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3419	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3641	. 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 2146  {crab 3418  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459

This theorem is used by:  elrab3  3653  elrabd  3654  elrabrd  3655  elrab2  3656  ralrab  3659  rexrab  3661  reurab  3666  rabsnt  4699  unimax  4912  ssintub  4933  intminss  4941  rabxfrd  5390  ssimaex  6970  weniso  7363  canth  7373  riotarab  7418  sorpsscmpl  7741  onnminsb  7804  dfom2  7870  ssnlim  7888  elsuppfng  8171  elsuppfn  8172  ressuppssdif  8187  oeeulem  8593  cofonr  8666  elpmg  8846  fineqvlem  9233  mapfienlem2  9373  supub  9426  suplub  9427  ordtypelem6  9492  ordtypelem7  9493  hartogslem1  9511  hartogs  9513  wemapsolem  9519  card2on  9523  elharval  9530  wdom2d  9549  cantnfs  9642  scottex  9869  scottexOLD  9870  scottelrankd  9884  tskwe  9952  cardid2  9955  iscard2  9978  cardmin2  10001  acni3  10047  alephsuc2  10080  kmlem1  10150  cofsmo  10268  coftr  10272  fin23lem11  10316  enfin2i  10320  fin1a2lem9  10407  fin1a2lem11  10409  axcc4  10438  axdc3lem2  10450  zorn2lem7  10501  ondomon  10562  alephval2  10572  grutsk  10822  negf1o  11659  infm3  12189  nnind  12266  peano2uz2  12700  peano5uzi  12701  dfuzi  12703  uzind  12704  uzind3  12706  eluz1  12882  uzind4  12946  nnwos  12955  eqreznegel  12974  zmin  12984  elixx1  13397  elioo2  13429  elfz1  13556  flval3  13866  serge0  14110  expge0  14152  expge1  14153  hashbclem  14507  pr2pwpr  14534  elss2prb  14543  hash2sspr  14544  wrdmap  14601  wwlktovfo  15019  shftf  15140  rlimrege0  15654  incexc2  15915  dvdsdivcl  16396  divalglem4  16476  divalgmod  16486  bitsval  16504  bezout  16623  dfgcd2  16626  lcmledvds  16679  lcmgcdlem  16686  lcmfledvds  16712  1nprm  16759  1idssfct  16760  isprm2  16762  hashdvds  16856  phisum  16872  odzval  16873  odzcllem  16874  odzdvds  16877  prmreclem2  16999  prmreclem5  17002  rami  17097  ramub1lem1  17108  ramub1lem2  17109  prmgaplem3  17135  prmgaplem4  17136  prmgaplem5  17137  prmgaplem6  17138  ismre  17664  ismri  17709  isacs  17729  isacs1i  17735  catlid  17761  catrid  17762  ismon  17812  isnat  18029  eldmcoa  18144  fncnvimaeqv  18198  lubeldm  18429  glbeldm  18442  gsumval2  18776  ismgmhm  18786  issubmgm  18792  rabsubmgmd  18794  mgmhmeql  18806  ismhm  18880  issubm  18898  issubmd  18901  mndind  18924  grplinv  19100  issubg  19236  isnsg  19265  cycsubg  19323  isgim  19376  isga  19405  elcntz  19436  elcntzsn  19439  symgfix2  19530  symgsssg  19581  symgfisg  19582  psgnunilem5  19608  odid  19652  odlem2  19653  gexid  19695  gexlem2  19696  gexdvds  19698  isslw  19722  pgpssslw  19728  pj1id  19813  oddvdssubg  19969  pgpfac1lem5  20195  ablfaclem2  20202  isirred  20547  isrnghm  20569  isrngim  20573  isrhm0  20604  isrim0  20611  rimval  20628  issubrng  20696  issubrg  20720  rgspnmin  20764  issdrg  20941  isabv  20964  islss  21105  islmhm  21198  islmim  21233  islbs  21247  isprmidl  21513  psgndiflemB  21800  elocv  21868  isobs  21920  dsmmelbas  21939  frlmelbas  21956  islinds  22009  gsumbagdiaglem  22131  rhmpsrlem2  22141  psrlidm  22161  psrridm  22162  psrass1  22163  psrcom  22167  mplsubglem  22198  mpllsslem  22199  evlsval2  22288  ismhp  22353  ismhp3  22355  mhpmulcl  22362  psdmul  22379  coe1ae0  22426  coe1mul2  22480  dmatel  22700  scmatel  22712  scmateALT  22719  symgmatr01lem  22860  pmatcoe1fsupp  22908  cpmatel  22918  chpscmat  23049  istopon  23119  fctop  23211  cctop  23213  ppttop  23214  pptbas  23215  epttop  23216  iscld  23234  clscld  23254  isnei  23310  neips  23320  neiptopnei  23339  iscn  23442  iscnp  23444  cmpsublem  23606  conncompconn  23639  2ndc1stc  23658  2ndcdisj  23664  elkgen  23744  xkoccn  23827  txdis1cn  23843  txkgen  23860  xkococnlem  23867  xkococn  23868  xkoinjcn  23895  txconn  23897  elqtop  23905  elmptrab  24035  fbssfi  24045  opnfbas  24050  elfg  24079  cfinfil  24101  csdfil  24102  supfil  24103  filssufilg  24119  uffix  24129  fixufil  24130  uffixfr  24131  elflim2  24172  fclscf  24233  flimfnfcls  24236  alexsubALTlem2  24256  alexsubALTlem4  24258  alexsubALT  24259  ptcmplem2  24261  elutop  24441  isucn  24485  iscfilu  24495  ispsmet  24512  ismet  24531  isxmet  24532  elblps  24595  elbl  24596  restmetu  24778  icccmp  25034  elcncf  25099  ishtpy  25182  isphtpy  25191  om1elbas  25242  iscfil  25475  iscau  25486  iscmet  25494  lmle  25511  rrxfsupp  25612  minveclem3  25639  minveclem4  25642  ovolshftlem1  25719  ovolscalem1  25723  ovolicc2lem3  25729  dyadmax  25808  dyadmbllem  25809  opnmbllem  25811  vitalilem2  25819  vitalilem3  25820  elcpn  26144  ig1pval3  26386  coelem  26434  quotlem  26512  elqaalem1  26531  elqaalem3  26533  aannenlem1  26542  aannenlem2  26543  dmarea  27173  jensen  27204  ftalem4  27291  efnnfsumcl  27318  efchtdvds  27374  sqff1o  27397  fsumdvdsdiaglem  27398  dvdsppwf1o  27401  dvdsflf1o  27402  dvdsflsumcom  27403  musum  27406  muinv  27408  logfac2  27432  dchrelbas  27451  lgsfle1  27521  lgsle1  27527  lgsdirprm  27546  lgsne0  27550  lgsquadlem1  27595  lgsquadlem2  27596  dchrvmasumlem1  27710  logsqvma  27757  pntleml  27826  ltsval2  27871  ltsres  27877  conway  28023  cutcuts  28025  cutbday  28028  cutsun12  28034  cutbdaybnd2  28040  cutbdaylt  28042  bday1  28058  cutlt  28176  precsexlem8  28458  precsexlem9  28459  precsexlem11  28461  oncutlt  28508  noseqinds  28537  peano5uzs  28648  uzsind  28649  tgellng  28873  mircgr  28985  mirbtwn  28986  elplng  29113  iseqlg  29239  ttgelitv  29287  upgrle  29495  upgrbi  29498  umgredg2  29505  umgrbi  29506  edgupgr  29539  edgumgr  29540  upgredg  29542  numedglnl  29549  edgusgr  29568  usgruspgrb  29591  usgredg2ALT  29601  ushgredgedg  29637  ushgredgedgloop  29639  usgrexmplef  29667  upgrreslem  29712  umgrreslem  29713  upgrres1  29721  nbgrel  29748  nbupgrel  29753  nbumgrvtx  29754  nbusgreledg  29761  nbgrnself  29767  uvtxusgrel  29811  vtxdgoddnumeven  29961  rgrusgrprc  29997  lfgrwlkprop  30097  iswwlks  30252  iswwlksn  30254  wwlksnextsurj  30316  rusgrnumwwlkslem  30388  rusgrnumwwlks  30393  isclwwlk  30402  clwwlknscsh  30480  eleclclwwlkn  30494  clwlknf1oclwwlkn  30502  clwwlkvbij  30531  eupth2lems  30660  konigsberglem4  30677  fusgreg2wsplem  30755  2clwwlkel  30771  extwwlkfabel  30775  clwwlknonclwlknonf1o  30784  dlwwlknondlwlknonf1o  30787  numclwwlk2lem1  30798  numclwlk2lem2f  30799  numclwlk2lem2f1o  30801  grpoidinv2  30938  grpoinv  30948  isssp  31147  islno  31176  isblo  31205  ishmo  31234  ubthlem1  31293  ubthlem2  31294  htthlem  31340  ocel  31704  shsval2i  31810  ococin  31831  chsupsn  31836  eleigvec  32380  cnlnadjlem5  32494  shatomistici  32784  hatomistici  32785  dmrab  32914  nnindf  33234  indf1ofs  33256  ismnt  33367  pwrssmgc  33384  tocycf  33501  tocyc01  33502  trsp2cyc  33507  cycpmco2f1  33508  cycpmco2rn  33509  cycpmco2lem2  33511  cycpmco2lem3  33512  cycpmco2lem5  33514  cycpmco2lem6  33515  cycpmco2lem7  33516  cycpmconjv  33526  tocyccntz  33528  cyc3evpm  33534  cycpmgcl  33537  cyc3conja  33541  isfxp  33552  fxpgaeq  33553  elrgspnsubrun  33633  rlocisunit  33660  fldgensdrg  33699  nsgmgclem  33784  nsgmgc  33785  nsgqusf1olem2  33787  ismxidl  33809  ssmxidl  33821  isrprm  33871  1arithufdlem3  33900  1arithufdlem4  33901  1arithufd  33902  mplvrpmlem  33997  mplvrpmga  33999  mplvrpmmhm  34000  fedgmullem2  34084  ply1annnr  34157  minplyann  34163  minplyirred  34165  constrsuc  34192  zarclsiin  34325  zart0  34333  rhmpreimacnlem  34338  ordtconnlem1  34378  sigagenval  34595  ldsysgenld  34615  ldgenpisyslem1  34618  ldgenpisyslem2  34619  ldgenpisys  34621  ddemeas  34691  ismbfm  34706  imambfm  34717  dya2iocuni  34738  oms0  34752  omssubadd  34755  elcarsg  34760  issibf  34788  sitgfval  34796  oddpwdc  34809  eulerpartlemgh  34833  eulerpartlemgs2  34835  dstfrvel  34929  ballotlemfc0  34948  ballotlemfcc  34949  ballotlemiex  34957  ballotlemfrcn0  34985  ballotlemirc  34987  ballotlem7  34991  reprsum  35065  reprsuc  35067  reprpmtf1o  35078  reprdifc  35079  fnrelpredd  35540  fineqvnttrclselem2  35592  connpconn  35764  iscvm  35788  cvmsi  35794  cvmsval  35795  cvmliftmolem2  35811  cvmliftiota  35830  snmlval  35860  satfv1lem  35891  fmlafvel  35914  fmla1  35916  fmlaomn0  35919  satfv0fvfmla0  35942  sategoelfvb  35948  elmpst  36065  lineelsb2  36677  linerflx1  36678  fwddifval  36691  fwddifnval  36692  rankeq1o  36700  finminlem  36886  fneint  36916  fnessref  36925  topmeet  36932  topjoin  36933  neifg  36939  weiunlem  37031  weiunfrlem  37032  weiunse  37036  regsfromregtco  37106  relowlssretop  38066  fin2solem  38314  fin2so  38315  poimirlem4  38332  poimirlem25  38353  poimirlem26  38354  poimirlem27  38355  poimirlem31  38359  poimirlem32  38360  opnmbllem0  38364  mblfinlem2  38366  itg2gt0cn  38383  indexa  38442  nninfnub  38460  istotbnd  38478  sstotbnd2  38483  isbnd  38489  isrngohom  38674  isrngoiso  38687  isidl  38723  ispridl  38743  ismaxidl  38749  prnc  38776  isfldidl  38777  islshp  39811  lssats  39844  islfl  39892  isat  40118  atlatmstc  40151  islln  40338  islpln  40362  islvol  40405  linepsubN  40584  elpmap  40590  pmapsub  40600  elpadd  40631  paddvaln0N  40633  islhp  40828  isldil  40942  isltrn  40951  isdilN  40986  istrnN  40989  diaval  41864  diaelval  41865  diaeldm  41868  diaelrnN  41877  cdlemm10N  41950  docaclN  41956  dibglbN  41998  dicval  42008  dicfnN  42015  dicvalrelN  42017  dihglblem2aN  42125  dihglblem2N  42126  dihglblem3N  42127  dih1dimatlem  42161  dihglb2  42174  dochvalr  42189  doch2val2  42196  dochocss  42198  islpolN  42315  mapd0  42497  aks4d1p4  42904  aks4d1p7  42908  isprimroot  42918  linvh  42921  primrootsunit1  42922  primrootscoprmpow  42924  primrootscoprbij  42927  sticksstones3  42973  aks6d1c6lem3  42997  grpods  43019  unitscyglem2  43021  unitscyglem4  43023  unitscyglem5  43024  supinf  43068  fsuppssindlem2  43382  infdesc  43433  isnacs  43493  elmzpcl  43515  mzpindd  43535  rencldnfilem  43605  irrapxlem6  43612  pellexlem3  43616  pellexlem5  43618  elpell1qr  43632  elpell14qr  43634  elpell1234qr  43636  pellfundre  43666  pellfundge  43667  pellfundlb  43669  pellfundglb  43670  rmspecnonsq  43692  jm2.22  43780  jm2.23  43781  rpnnen3lem  43816  fnwe2lem2  43836  elmnc  43921  dgraalem  43930  dgraaub  43933  mpaalem  43937  onsucelab  44048  limnsuc  44050  sqrtcvallem1  44415  rfovcnvf1od  44788  nzss  45085  iccshift  46292  iooshift  46296  limcperiod  46402  sumnnodd  46404  ioodvbdlimc1lem1  46703  dvnprodlem1  46718  dvnprodlem3  46720  itgperiod  46753  stoweidlem14  46786  stoweidlem15  46787  stoweidlem16  46788  stoweidlem31  46803  stoweidlem36  46808  stoweidlem46  46818  stoweidlem48  46820  fourierdlem2  46881  fourierdlem3  46882  fourierdlem20  46899  fourierdlem25  46904  fourierdlem37  46916  fourierdlem42  46921  fourierdlem48  46926  fourierdlem51  46929  fourierdlem63  46941  fourierdlem64  46942  fourierdlem65  46943  fourierdlem79  46957  fourierdlem81  46959  elaa2lem  47005  etransclem24  47030  etransclem26  47032  etransclem28  47034  etransclem35  47041  etransclem48  47054  salgenval  47093  salgenn0  47103  salgencl  47104  sssalgen  47107  salgenss  47108  salgenuni  47109  issalgend  47110  salgencntex  47115  subsaliuncllem  47129  sge0fodjrnlem  47188  meadjiunlem  47237  caragenel  47267  ovnlecvr  47330  ovnpnfelsup  47331  ovncvrrp  47336  ovnsubaddlem1  47342  hoidmv1lelem1  47363  hoidmv1lelem2  47364  hoidmv1lelem3  47365  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem4  47370  ovnhoilem1  47373  ovnlecvr2  47382  ovncvr2  47383  issmflem  47499  smflimlem2  47544  smflimlem3  47545  smflimsuplem2  47593  elsetpreimafvrab  48201  iccpart  48223  sprel  48291  prelspr  48293  sprsymrelfolem2  48300  sprsymrelf  48302  prpair  48308  paireqne  48318  prprelb  48323  prprelprb  48324  dfodd2  48459  dfeven5  48489  dfodd7  48490  fpprel  48551  clnbgrel  48651  clnbupgrel  48657  sclnbgrel  48670  vopnbgrel  48677  dfclnbgr6  48679  dfnbgr6  48680  isubgredg  48689  uhgrimisgrgric  48754  grtriprop  48764  isgrtri  48766  stgredgel  48780  stgrusgra  48782  uspgrlimlem3  48813  uspgrlim  48815  grlimgredgex  48823  grlimgrtrilem2  48825  gpgiedgdmel  48872  gpgedgel  48873  gpgnbgrvtx0  48897  gpgnbgrvtx1  48898  gpgprismgr4cycllem10  48927  1hegrlfgr  48955  assintop  49031  isassintop  49032  assintopcllaw  49034  0even  49059  2even  49061  2zrngamgm  49067  dmatALTbasel  49239  lcoval  49249  elbigo  49388  elrrx2linest2  49582  itsclc0  49608  itsclc0b  49609  itscnhlinecirc02p  49622  unilbss  49653  secval  50582  cscval  50583  cotval  50584