Theorem elrab 3647

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {crab 3395  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438

This theorem is referenced by:  elrab3  3648  elrabd  3649  elrab2  3650  ralrab  3653  rexrab  3655  reurab  3660  rabsnt  4684  unimax  4895  ssintub  4916  intminss  4924  rabxfrd  5355  ssimaex  6907  weniso  7288  canth  7300  riotarab  7345  sorpsscmpl  7667  onnminsb  7732  dfom2  7798  ssnlim  7816  elsuppfng  8099  elsuppfn  8100  ressuppssdif  8115  oeeulem  8516  cofonr  8589  elpmg  8767  fineqvlem  9150  mapfienlem2  9290  supub  9343  suplub  9344  ordtypelem6  9409  ordtypelem7  9410  hartogslem1  9428  hartogs  9430  wemapsolem  9436  card2on  9440  elharval  9447  wdom2d  9466  cantnfs  9556  scottex  9778  tskwe  9843  cardid2  9846  iscard2  9869  cardmin2  9892  acni3  9938  alephsuc2  9971  kmlem1  10042  cofsmo  10160  coftr  10164  fin23lem11  10208  enfin2i  10212  fin1a2lem9  10299  fin1a2lem11  10301  axcc4  10330  axdc3lem2  10342  zorn2lem7  10393  ondomon  10454  alephval2  10463  grutsk  10713  negf1o  11547  infm3  12081  nnind  12143  peano2uz2  12561  peano5uzi  12562  dfuzi  12564  uzind  12565  uzind3  12567  eluz1  12736  uzind4  12804  nnwos  12813  eqreznegel  12832  zmin  12842  elixx1  13254  elioo2  13286  elfz1  13412  flval3  13719  serge0  13963  expge0  14005  expge1  14006  hashbclem  14359  pr2pwpr  14386  elss2prb  14395  hash2sspr  14396  wrdmap  14453  wwlktovfo  14865  shftf  14986  rlimrege0  15486  incexc2  15745  dvdsdivcl  16227  divalglem4  16307  divalgmod  16317  bitsval  16335  bezout  16454  dfgcd2  16457  lcmledvds  16510  lcmgcdlem  16517  lcmfledvds  16543  1nprm  16590  1idssfct  16591  isprm2  16593  hashdvds  16686  phisum  16702  odzval  16703  odzcllem  16704  odzdvds  16707  prmreclem2  16829  prmreclem5  16832  rami  16927  ramub1lem1  16938  ramub1lem2  16939  prmgaplem3  16965  prmgaplem4  16966  prmgaplem5  16967  prmgaplem6  16968  ismre  17492  ismri  17537  isacs  17557  isacs1i  17563  catlid  17589  catrid  17590  ismon  17640  isnat  17857  eldmcoa  17972  fncnvimaeqv  18026  lubeldm  18257  glbeldm  18270  gsumval2  18594  ismgmhm  18604  issubmgm  18610  rabsubmgmd  18612  mgmhmeql  18624  ismhm  18693  issubm  18711  issubmd  18714  mndind  18736  grplinv  18902  issubg  19039  isnsg  19068  cycsubg  19121  isgim  19175  isga  19204  elcntz  19235  elcntzsn  19238  symgfix2  19329  symgsssg  19380  symgfisg  19381  psgnunilem5  19407  odid  19451  odlem2  19452  gexid  19494  gexlem2  19495  gexdvds  19497  isslw  19521  pgpssslw  19527  pj1id  19612  oddvdssubg  19768  pgpfac1lem5  19994  ablfaclem2  20001  isirred  20338  isrnghm  20360  isrngim  20364  isrim0  20401  issubrng  20463  issubrg  20487  rgspnmin  20531  issdrg  20704  isabv  20727  islss  20868  islmhm  20962  islmim  20997  islbs  21011  psgndiflemB  21538  elocv  21606  isobs  21658  dsmmelbas  21677  frlmelbas  21694  islinds  21747  gsumbagdiaglem  21868  rhmpsrlem2  21879  psrlidm  21900  psrridm  21901  psrass1  21902  psrcom  21906  mplsubglem  21937  mpllsslem  21938  evlsval2  22023  ismhp  22056  ismhp3  22058  mhpmulcl  22065  psdmul  22082  coe1ae0  22130  coe1mul2  22184  dmatel  22409  scmatel  22421  scmateALT  22428  symgmatr01lem  22569  pmatcoe1fsupp  22617  cpmatel  22627  chpscmat  22758  istopon  22828  fctop  22920  cctop  22922  ppttop  22923  pptbas  22924  epttop  22925  iscld  22943  clscld  22963  isnei  23019  neips  23029  neiptopnei  23048  iscn  23151  iscnp  23153  cmpsublem  23315  conncompconn  23348  2ndc1stc  23367  2ndcdisj  23372  elkgen  23452  xkoccn  23535  txdis1cn  23551  txkgen  23568  xkococnlem  23575  xkococn  23576  xkoinjcn  23603  txconn  23605  elqtop  23613  elmptrab  23743  fbssfi  23753  opnfbas  23758  elfg  23787  cfinfil  23809  csdfil  23810  supfil  23811  filssufilg  23827  uffix  23837  fixufil  23838  uffixfr  23839  elflim2  23880  fclscf  23941  flimfnfcls  23944  alexsubALTlem2  23964  alexsubALTlem4  23966  alexsubALT  23967  ptcmplem2  23969  elutop  24149  isucn  24193  iscfilu  24203  ispsmet  24220  ismet  24239  isxmet  24240  elblps  24303  elbl  24304  restmetu  24486  icccmp  24742  elcncf  24810  ishtpy  24899  isphtpy  24908  om1elbas  24960  iscfil  25193  iscau  25204  iscmet  25212  lmle  25229  rrxfsupp  25330  minveclem3  25357  minveclem4  25360  ovolshftlem1  25438  ovolscalem1  25442  ovolicc2lem3  25448  dyadmax  25527  dyadmbllem  25528  opnmbllem  25530  vitalilem2  25538  vitalilem3  25539  elcpn  25864  ig1pval3  26111  coelem  26159  quotlem  26236  elqaalem1  26255  elqaalem3  26257  aannenlem1  26264  aannenlem2  26265  dmarea  26895  jensen  26927  ftalem4  27014  efnnfsumcl  27041  efchtdvds  27097  sqff1o  27120  fsumdvdsdiaglem  27121  dvdsppwf1o  27124  dvdsflf1o  27125  dvdsflsumcom  27126  musum  27129  muinv  27131  logfac2  27156  dchrelbas  27175  lgsfle1  27245  lgsle1  27251  lgsdirprm  27270  lgsne0  27274  lgsquadlem1  27319  lgsquadlem2  27320  dchrvmasumlem1  27434  logsqvma  27481  pntleml  27550  sltval2  27596  sltres  27602  conway  27741  scutcut  27743  scutbday  27746  scutun12  27752  scutbdaybnd2  27758  scutbdaylt  27760  bday1s  27776  cutlt  27877  precsexlem8  28153  precsexlem9  28154  precsexlem11  28156  onscutlt  28202  noseqinds  28224  peano5uzs  28329  uzsind  28330  tgellng  28532  mircgr  28636  mirbtwn  28637  iseqlg  28846  ttgelitv  28862  upgrle  29069  upgrbi  29072  umgredg2  29079  umgrbi  29080  edgupgr  29113  edgumgr  29114  upgredg  29116  numedglnl  29123  edgusgr  29139  usgruspgrb  29162  usgredg2ALT  29172  ushgredgedg  29208  ushgredgedgloop  29210  usgrexmplef  29238  upgrreslem  29283  umgrreslem  29284  upgrres1  29292  nbgrel  29319  nbupgrel  29324  nbumgrvtx  29325  nbusgreledg  29332  nbgrnself  29338  uvtxusgrel  29382  vtxdgoddnumeven  29533  rgrusgrprc  29569  lfgrwlkprop  29665  iswwlks  29815  iswwlksn  29817  wwlksnextsurj  29879  rusgrnumwwlkslem  29948  rusgrnumwwlks  29953  isclwwlk  29962  clwwlknscsh  30040  eleclclwwlkn  30054  clwlknf1oclwwlkn  30062  clwwlkvbij  30091  eupth2lems  30216  konigsberglem4  30233  fusgreg2wsplem  30311  2clwwlkel  30327  extwwlkfabel  30331  clwwlknonclwlknonf1o  30340  dlwwlknondlwlknonf1o  30343  numclwwlk2lem1  30354  numclwlk2lem2f  30355  numclwlk2lem2f1o  30357  grpoidinv2  30493  grpoinv  30503  isssp  30702  islno  30731  isblo  30760  ishmo  30789  ubthlem1  30848  ubthlem2  30849  htthlem  30895  ocel  31259  shsval2i  31365  ococin  31386  chsupsn  31391  eleigvec  31935  cnlnadjlem5  32049  shatomistici  32339  hatomistici  32340  dmrab  32474  elrabrd  32476  nnindf  32800  indf1ofs  32845  ismnt  32962  pwrssmgc  32979  tocycf  33084  tocyc01  33085  trsp2cyc  33090  cycpmco2f1  33091  cycpmco2rn  33092  cycpmco2lem2  33094  cycpmco2lem3  33095  cycpmco2lem5  33097  cycpmco2lem6  33098  cycpmco2lem7  33099  cycpmconjv  33109  tocyccntz  33111  cyc3evpm  33117  cycpmgcl  33120  cycpmconjslem2  33122  cyc3conja  33124  isfxp  33135  fxpgaeq  33136  elrgspnsubrun  33214  fldgensdrg  33278  nsgmgclem  33374  nsgmgc  33375  nsgqusf1olem2  33377  isprmidl  33401  ismxidl  33425  ssmxidl  33437  isrprm  33480  1arithufdlem3  33509  1arithufdlem4  33510  1arithufd  33511  mplvrpmlem  33571  mplvrpmga  33573  mplvrpmmhm  33574  fedgmullem2  33641  ply1annnr  33714  minplyann  33720  minplyirred  33722  constrsuc  33749  zarclsiin  33882  zart0  33890  rhmpreimacnlem  33895  ordtconnlem1  33935  sigagenval  34151  ldsysgenld  34171  ldgenpisyslem1  34174  ldgenpisyslem2  34175  ldgenpisys  34177  ddemeas  34247  ismbfm  34262  imambfm  34273  dya2iocuni  34294  oms0  34308  omssubadd  34311  elcarsg  34316  issibf  34344  sitgfval  34352  oddpwdc  34365  eulerpartlemgh  34389  eulerpartlemgs2  34391  dstfrvel  34485  ballotlemfc0  34504  ballotlemfcc  34505  ballotlemiex  34513  ballotlemfrcn0  34541  ballotlemirc  34543  ballotlem7  34547  reprsum  34624  reprsuc  34626  reprpmtf1o  34637  reprdifc  34638  fnrelpredd  35100  fineqvnttrclselem2  35140  connpconn  35277  iscvm  35301  cvmsi  35307  cvmsval  35308  cvmliftmolem2  35324  cvmliftiota  35343  snmlval  35373  satfv1lem  35404  fmlafvel  35427  fmla1  35429  fmlaomn0  35432  satfv0fvfmla0  35455  sategoelfvb  35461  elmpst  35578  lineelsb2  36188  linerflx1  36189  fwddifval  36202  fwddifnval  36203  rankeq1o  36211  finminlem  36358  fneint  36388  fnessref  36397  topmeet  36404  topjoin  36405  neifg  36411  weiunlem2  36503  weiunfrlem  36504  weiunse  36508  relowlssretop  37403  fin2solem  37652  fin2so  37653  poimirlem4  37670  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem31  37697  poimirlem32  37698  opnmbllem0  37702  mblfinlem2  37704  itg2gt0cn  37721  indexa  37779  nninfnub  37797  istotbnd  37815  sstotbnd2  37820  isbnd  37826  isrngohom  38011  isrngoiso  38024  isidl  38060  ispridl  38080  ismaxidl  38086  prnc  38113  isfldidl  38114  islshp  39024  lssats  39057  islfl  39105  isat  39331  atlatmstc  39364  islln  39551  islpln  39575  islvol  39618  linepsubN  39797  elpmap  39803  pmapsub  39813  elpadd  39844  paddvaln0N  39846  islhp  40041  isldil  40155  isltrn  40164  isdilN  40199  istrnN  40202  diaval  41077  diaelval  41078  diaeldm  41081  diaelrnN  41090  cdlemm10N  41163  docaclN  41169  dibglbN  41211  dicval  41221  dicfnN  41228  dicvalrelN  41230  dihglblem2aN  41338  dihglblem2N  41339  dihglblem3N  41340  dih1dimatlem  41374  dihglb2  41387  dochvalr  41402  doch2val2  41409  dochocss  41411  islpolN  41528  mapd0  41710  aks4d1p4  42118  aks4d1p7  42122  isprimroot  42132  linvh  42135  primrootsunit1  42136  primrootscoprmpow  42138  primrootscoprbij  42141  sticksstones3  42187  aks6d1c6lem3  42211  grpods  42233  unitscyglem2  42235  unitscyglem4  42237  unitscyglem5  42238  supinf  42281  fsuppssindlem2  42631  infdesc  42682  isnacs  42743  elmzpcl  42765  mzpindd  42785  rencldnfilem  42859  irrapxlem6  42866  pellexlem3  42870  pellexlem5  42872  elpell1qr  42886  elpell14qr  42888  elpell1234qr  42890  pellfundre  42920  pellfundge  42921  pellfundlb  42923  pellfundglb  42924  rmspecnonsq  42946  jm2.22  43034  jm2.23  43035  rpnnen3lem  43070  fnwe2lem2  43090  elmnc  43175  dgraalem  43184  dgraaub  43187  mpaalem  43191  onsucelab  43302  limnsuc  43304  sqrtcvallem1  43670  rfovcnvf1od  44043  scottelrankd  44286  nzss  44356  iccshift  45564  iooshift  45568  limcperiod  45674  sumnnodd  45676  ioodvbdlimc1lem1  45975  dvnprodlem1  45990  dvnprodlem3  45992  itgperiod  46025  stoweidlem14  46058  stoweidlem15  46059  stoweidlem16  46060  stoweidlem31  46075  stoweidlem36  46080  stoweidlem46  46090  stoweidlem48  46092  fourierdlem2  46153  fourierdlem3  46154  fourierdlem20  46171  fourierdlem25  46176  fourierdlem37  46188  fourierdlem42  46193  fourierdlem48  46198  fourierdlem51  46201  fourierdlem63  46213  fourierdlem64  46214  fourierdlem65  46215  fourierdlem79  46229  fourierdlem81  46231  elaa2lem  46277  etransclem24  46302  etransclem26  46304  etransclem28  46306  etransclem35  46313  etransclem48  46326  salgenval  46365  salgenn0  46375  salgencl  46376  sssalgen  46379  salgenss  46380  salgenuni  46381  issalgend  46382  salgencntex  46387  subsaliuncllem  46401  sge0fodjrnlem  46460  meadjiunlem  46509  caragenel  46539  ovnlecvr  46602  ovnpnfelsup  46603  ovncvrrp  46608  ovnsubaddlem1  46614  hoidmv1lelem1  46635  hoidmv1lelem2  46636  hoidmv1lelem3  46637  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem4  46642  ovnhoilem1  46645  ovnlecvr2  46654  ovncvr2  46655  issmflem  46771  smflimlem2  46816  smflimlem3  46817  smflimsuplem2  46865  elsetpreimafvrab  47431  iccpart  47453  sprel  47521  prelspr  47523  sprsymrelfolem2  47530  sprsymrelf  47532  prpair  47538  paireqne  47548  prprelb  47553  prprelprb  47554  dfodd2  47673  dfeven5  47703  dfodd7  47704  fpprel  47765  clnbgrel  47865  clnbupgrel  47871  sclnbgrel  47884  vopnbgrel  47891  dfclnbgr6  47893  dfnbgr6  47894  isubgredg  47903  uhgrimisgrgric  47968  grtriprop  47978  isgrtri  47980  stgredgel  47994  stgrusgra  47996  uspgrlimlem3  48027  uspgrlim  48029  grlimgredgex  48037  grlimgrtrilem2  48039  gpgiedgdmel  48086  gpgedgel  48087  gpgnbgrvtx0  48111  gpgnbgrvtx1  48112  gpgprismgr4cycllem10  48141  1hegrlfgr  48169  assintop  48246  isassintop  48247  assintopcllaw  48249  0even  48274  2even  48276  2zrngamgm  48282  dmatALTbasel  48440  lcoval  48450  elbigo  48589  elrrx2linest2  48783  itsclc0  48809  itsclc0b  48810  itscnhlinecirc02p  48823  unilbss  48855  secval  49785  cscval  49786  cotval  49787