Theorem elrab 3634

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3389  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431

This theorem is referenced by:  elrab3  3635  elrabd  3636  elrab2  3637  ralrab  3640  rexrab  3642  reurab  3647  rabsnt  4675  unimax  4887  ssintub  4908  intminss  4916  rabxfrd  5359  ssimaex  6925  weniso  7309  canth  7321  riotarab  7366  sorpsscmpl  7688  onnminsb  7753  dfom2  7819  ssnlim  7837  elsuppfng  8119  elsuppfn  8120  ressuppssdif  8135  oeeulem  8537  cofonr  8610  elpmg  8790  fineqvlem  9176  mapfienlem2  9319  supub  9372  suplub  9373  ordtypelem6  9438  ordtypelem7  9439  hartogslem1  9457  hartogs  9459  wemapsolem  9465  card2on  9469  elharval  9476  wdom2d  9495  cantnfs  9587  scottex  9809  tskwe  9874  cardid2  9877  iscard2  9900  cardmin2  9923  acni3  9969  alephsuc2  10002  kmlem1  10073  cofsmo  10191  coftr  10195  fin23lem11  10239  enfin2i  10243  fin1a2lem9  10330  fin1a2lem11  10332  axcc4  10361  axdc3lem2  10373  zorn2lem7  10424  ondomon  10485  alephval2  10495  grutsk  10745  negf1o  11580  infm3  12115  nnind  12192  peano2uz2  12617  peano5uzi  12618  dfuzi  12620  uzind  12621  uzind3  12623  eluz1  12792  uzind4  12856  nnwos  12865  eqreznegel  12884  zmin  12894  elixx1  13307  elioo2  13339  elfz1  13466  flval3  13774  serge0  14018  expge0  14060  expge1  14061  hashbclem  14414  pr2pwpr  14441  elss2prb  14450  hash2sspr  14451  wrdmap  14508  wwlktovfo  14920  shftf  15041  rlimrege0  15541  incexc2  15803  dvdsdivcl  16285  divalglem4  16365  divalgmod  16375  bitsval  16393  bezout  16512  dfgcd2  16515  lcmledvds  16568  lcmgcdlem  16575  lcmfledvds  16601  1nprm  16648  1idssfct  16649  isprm2  16651  hashdvds  16745  phisum  16761  odzval  16762  odzcllem  16763  odzdvds  16766  prmreclem2  16888  prmreclem5  16891  rami  16986  ramub1lem1  16997  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  ismre  17552  ismri  17597  isacs  17617  isacs1i  17623  catlid  17649  catrid  17650  ismon  17700  isnat  17917  eldmcoa  18032  fncnvimaeqv  18086  lubeldm  18317  glbeldm  18330  gsumval2  18654  ismgmhm  18664  issubmgm  18670  rabsubmgmd  18672  mgmhmeql  18684  ismhm  18753  issubm  18771  issubmd  18774  mndind  18796  grplinv  18965  issubg  19102  isnsg  19130  cycsubg  19183  isgim  19237  isga  19266  elcntz  19297  elcntzsn  19300  symgfix2  19391  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  odid  19513  odlem2  19514  gexid  19556  gexlem2  19557  gexdvds  19559  isslw  19583  pgpssslw  19589  pj1id  19674  oddvdssubg  19830  pgpfac1lem5  20056  ablfaclem2  20063  isirred  20399  isrnghm  20421  isrngim  20425  isrim0  20462  issubrng  20524  issubrg  20548  rgspnmin  20592  issdrg  20765  isabv  20788  islss  20929  islmhm  21022  islmim  21057  islbs  21071  psgndiflemB  21580  elocv  21648  isobs  21700  dsmmelbas  21719  frlmelbas  21736  islinds  21789  gsumbagdiaglem  21910  rhmpsrlem2  21920  psrlidm  21940  psrridm  21941  psrass1  21942  psrcom  21946  mplsubglem  21977  mpllsslem  21978  evlsval2  22065  ismhp  22106  ismhp3  22108  mhpmulcl  22115  psdmul  22132  coe1ae0  22180  coe1mul2  22234  dmatel  22458  scmatel  22470  scmateALT  22477  symgmatr01lem  22618  pmatcoe1fsupp  22666  cpmatel  22676  chpscmat  22807  istopon  22877  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  epttop  22974  iscld  22992  clscld  23012  isnei  23068  neips  23078  neiptopnei  23097  iscn  23200  iscnp  23202  cmpsublem  23364  conncompconn  23397  2ndc1stc  23416  2ndcdisj  23421  elkgen  23501  xkoccn  23584  txdis1cn  23600  txkgen  23617  xkococnlem  23624  xkococn  23625  xkoinjcn  23652  txconn  23654  elqtop  23662  elmptrab  23792  fbssfi  23802  opnfbas  23807  elfg  23836  cfinfil  23858  csdfil  23859  supfil  23860  filssufilg  23876  uffix  23886  fixufil  23887  uffixfr  23888  elflim2  23929  fclscf  23990  flimfnfcls  23993  alexsubALTlem2  24013  alexsubALTlem4  24015  alexsubALT  24016  ptcmplem2  24018  elutop  24198  isucn  24242  iscfilu  24252  ispsmet  24269  ismet  24288  isxmet  24289  elblps  24352  elbl  24353  restmetu  24535  icccmp  24791  elcncf  24856  ishtpy  24939  isphtpy  24948  om1elbas  24999  iscfil  25232  iscau  25243  iscmet  25251  lmle  25268  rrxfsupp  25369  minveclem3  25396  minveclem4  25399  ovolshftlem1  25476  ovolscalem1  25480  ovolicc2lem3  25486  dyadmax  25565  dyadmbllem  25566  opnmbllem  25568  vitalilem2  25576  vitalilem3  25577  elcpn  25901  ig1pval3  26143  coelem  26191  quotlem  26266  elqaalem1  26285  elqaalem3  26287  aannenlem1  26294  aannenlem2  26295  dmarea  26921  jensen  26952  ftalem4  27039  efnnfsumcl  27066  efchtdvds  27122  sqff1o  27145  fsumdvdsdiaglem  27146  dvdsppwf1o  27149  dvdsflf1o  27150  dvdsflsumcom  27151  musum  27154  muinv  27156  logfac2  27180  dchrelbas  27199  lgsfle1  27269  lgsle1  27275  lgsdirprm  27294  lgsne0  27298  lgsquadlem1  27343  lgsquadlem2  27344  dchrvmasumlem1  27458  logsqvma  27505  pntleml  27574  ltsval2  27620  ltsres  27626  conway  27771  cutcuts  27773  cutbday  27776  cutsun12  27782  cutbdaybnd2  27788  cutbdaylt  27790  bday1  27806  cutlt  27924  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  oncutlt  28256  noseqinds  28285  peano5uzs  28396  uzsind  28397  tgellng  28621  mircgr  28725  mirbtwn  28726  iseqlg  28935  ttgelitv  28951  upgrle  29159  upgrbi  29162  umgredg2  29169  umgrbi  29170  edgupgr  29203  edgumgr  29204  upgredg  29206  numedglnl  29213  edgusgr  29229  usgruspgrb  29252  usgredg2ALT  29262  ushgredgedg  29298  ushgredgedgloop  29300  usgrexmplef  29328  upgrreslem  29373  umgrreslem  29374  upgrres1  29382  nbgrel  29409  nbupgrel  29414  nbumgrvtx  29415  nbusgreledg  29422  nbgrnself  29428  uvtxusgrel  29472  vtxdgoddnumeven  29622  rgrusgrprc  29658  lfgrwlkprop  29754  iswwlks  29904  iswwlksn  29906  wwlksnextsurj  29968  rusgrnumwwlkslem  30040  rusgrnumwwlks  30045  isclwwlk  30054  clwwlknscsh  30132  eleclclwwlkn  30146  clwlknf1oclwwlkn  30154  clwwlkvbij  30183  eupth2lems  30308  konigsberglem4  30325  fusgreg2wsplem  30403  2clwwlkel  30419  extwwlkfabel  30423  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1o  30435  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  grpoidinv2  30586  grpoinv  30596  isssp  30795  islno  30824  isblo  30853  ishmo  30882  ubthlem1  30941  ubthlem2  30942  htthlem  30988  ocel  31352  shsval2i  31458  ococin  31479  chsupsn  31484  eleigvec  32028  cnlnadjlem5  32142  shatomistici  32432  hatomistici  32433  dmrab  32566  elrabrd  32568  nnindf  32893  indf1ofs  32926  ismnt  33043  pwrssmgc  33060  tocycf  33178  tocyc01  33179  trsp2cyc  33184  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmconjv  33203  tocyccntz  33205  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  isfxp  33229  fxpgaeq  33230  elrgspnsubrun  33310  fldgensdrg  33375  nsgmgclem  33471  nsgmgc  33472  nsgqusf1olem2  33474  isprmidl  33498  ismxidl  33522  ssmxidl  33534  isrprm  33577  1arithufdlem3  33606  1arithufdlem4  33607  1arithufd  33608  mplvrpmlem  33687  mplvrpmga  33689  mplvrpmmhm  33690  fedgmullem2  33774  ply1annnr  33847  minplyann  33853  minplyirred  33855  constrsuc  33882  zarclsiin  34015  zart0  34023  rhmpreimacnlem  34028  ordtconnlem1  34068  sigagenval  34284  ldsysgenld  34304  ldgenpisyslem1  34307  ldgenpisyslem2  34308  ldgenpisys  34310  ddemeas  34380  ismbfm  34395  imambfm  34406  dya2iocuni  34427  oms0  34441  omssubadd  34444  elcarsg  34449  issibf  34477  sitgfval  34485  oddpwdc  34498  eulerpartlemgh  34522  eulerpartlemgs2  34524  dstfrvel  34618  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemiex  34646  ballotlemfrcn0  34674  ballotlemirc  34676  ballotlem7  34680  reprsum  34757  reprsuc  34759  reprpmtf1o  34770  reprdifc  34771  fnrelpredd  35234  fineqvnttrclselem2  35266  connpconn  35417  iscvm  35441  cvmsi  35447  cvmsval  35448  cvmliftmolem2  35464  cvmliftiota  35483  snmlval  35513  satfv1lem  35544  fmlafvel  35567  fmla1  35569  fmlaomn0  35572  satfv0fvfmla0  35595  sategoelfvb  35601  elmpst  35718  lineelsb2  36330  linerflx1  36331  fwddifval  36344  fwddifnval  36345  rankeq1o  36353  finminlem  36500  fneint  36530  fnessref  36539  topmeet  36546  topjoin  36547  neifg  36553  weiunlem  36645  weiunfrlem  36646  weiunse  36650  regsfromregtco  36720  relowlssretop  37679  fin2solem  37927  fin2so  37928  poimirlem4  37945  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  opnmbllem0  37977  mblfinlem2  37979  itg2gt0cn  37996  indexa  38054  nninfnub  38072  istotbnd  38090  sstotbnd2  38095  isbnd  38101  isrngohom  38286  isrngoiso  38299  isidl  38335  ispridl  38355  ismaxidl  38361  prnc  38388  isfldidl  38389  islshp  39425  lssats  39458  islfl  39506  isat  39732  atlatmstc  39765  islln  39952  islpln  39976  islvol  40019  linepsubN  40198  elpmap  40204  pmapsub  40214  elpadd  40245  paddvaln0N  40247  islhp  40442  isldil  40556  isltrn  40565  isdilN  40600  istrnN  40603  diaval  41478  diaelval  41479  diaeldm  41482  diaelrnN  41491  cdlemm10N  41564  docaclN  41570  dibglbN  41612  dicval  41622  dicfnN  41629  dicvalrelN  41631  dihglblem2aN  41739  dihglblem2N  41740  dihglblem3N  41741  dih1dimatlem  41775  dihglb2  41788  dochvalr  41803  doch2val2  41810  dochocss  41812  islpolN  41929  mapd0  42111  aks4d1p4  42518  aks4d1p7  42522  isprimroot  42532  linvh  42535  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  sticksstones3  42587  aks6d1c6lem3  42611  grpods  42633  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  supinf  42681  fsuppssindlem2  43025  infdesc  43076  isnacs  43136  elmzpcl  43158  mzpindd  43178  rencldnfilem  43248  irrapxlem6  43255  pellexlem3  43259  pellexlem5  43261  elpell1qr  43275  elpell14qr  43277  elpell1234qr  43279  pellfundre  43309  pellfundge  43310  pellfundlb  43312  pellfundglb  43313  rmspecnonsq  43335  jm2.22  43423  jm2.23  43424  rpnnen3lem  43459  fnwe2lem2  43479  elmnc  43564  dgraalem  43573  dgraaub  43576  mpaalem  43580  onsucelab  43691  limnsuc  43693  sqrtcvallem1  44058  rfovcnvf1od  44431  scottelrankd  44674  nzss  44744  iccshift  45948  iooshift  45952  limcperiod  46058  sumnnodd  46060  ioodvbdlimc1lem1  46359  dvnprodlem1  46374  dvnprodlem3  46376  itgperiod  46409  stoweidlem14  46442  stoweidlem15  46443  stoweidlem16  46444  stoweidlem31  46459  stoweidlem36  46464  stoweidlem46  46474  stoweidlem48  46476  fourierdlem2  46537  fourierdlem3  46538  fourierdlem20  46555  fourierdlem25  46560  fourierdlem37  46572  fourierdlem42  46577  fourierdlem48  46582  fourierdlem51  46585  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem79  46613  fourierdlem81  46615  elaa2lem  46661  etransclem24  46686  etransclem26  46688  etransclem28  46690  etransclem35  46697  etransclem48  46710  salgenval  46749  salgenn0  46759  salgencl  46760  sssalgen  46763  salgenss  46764  salgenuni  46765  issalgend  46766  salgencntex  46771  subsaliuncllem  46785  sge0fodjrnlem  46844  meadjiunlem  46893  caragenel  46923  ovnlecvr  46986  ovnpnfelsup  46987  ovncvrrp  46992  ovnsubaddlem1  46998  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem4  47026  ovnhoilem1  47029  ovnlecvr2  47038  ovncvr2  47039  issmflem  47155  smflimlem2  47200  smflimlem3  47201  smflimsuplem2  47249  elsetpreimafvrab  47854  iccpart  47876  sprel  47944  prelspr  47946  sprsymrelfolem2  47953  sprsymrelf  47955  prpair  47961  paireqne  47971  prprelb  47976  prprelprb  47977  dfodd2  48112  dfeven5  48142  dfodd7  48143  fpprel  48204  clnbgrel  48304  clnbupgrel  48310  sclnbgrel  48323  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  isubgredg  48342  uhgrimisgrgric  48407  grtriprop  48417  isgrtri  48419  stgredgel  48433  stgrusgra  48435  uspgrlimlem3  48466  uspgrlim  48468  grlimgredgex  48476  grlimgrtrilem2  48478  gpgiedgdmel  48525  gpgedgel  48526  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  gpgprismgr4cycllem10  48580  1hegrlfgr  48608  assintop  48685  isassintop  48686  assintopcllaw  48688  0even  48713  2even  48715  2zrngamgm  48721  dmatALTbasel  48878  lcoval  48888  elbigo  49027  elrrx2linest2  49221  itsclc0  49247  itsclc0b  49248  itscnhlinecirc02p  49261  unilbss  49293  secval  50222  cscval  50223  cotval  50224