Theorem elrab 3631

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  {crab 3393  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435

This theorem is referenced by:  elrab3  3632  elrabd  3633  elrab2  3634  ralrab  3637  rexrab  3639  reurab  3644  rabsnt  4666  unimax  4878  ssintub  4899  intminss  4907  rabxfrd  5349  ssimaex  6916  weniso  7302  canth  7314  riotarab  7359  sorpsscmpl  7681  onnminsb  7746  dfom2  7812  ssnlim  7830  elsuppfng  8113  elsuppfn  8114  ressuppssdif  8129  oeeulem  8531  cofonr  8604  elpmg  8784  fineqvlem  9170  mapfienlem2  9313  supub  9366  suplub  9367  ordtypelem6  9432  ordtypelem7  9433  hartogslem1  9451  hartogs  9453  wemapsolem  9459  card2on  9463  elharval  9470  wdom2d  9489  cantnfs  9582  scottex  9804  tskwe  9869  cardid2  9872  iscard2  9895  cardmin2  9918  acni3  9964  alephsuc2  9997  kmlem1  10068  cofsmo  10186  coftr  10190  fin23lem11  10234  enfin2i  10238  fin1a2lem9  10325  fin1a2lem11  10327  axcc4  10356  axdc3lem2  10368  zorn2lem7  10419  ondomon  10480  alephval2  10490  grutsk  10740  negf1o  11575  infm3  12110  nnind  12187  peano2uz2  12612  peano5uzi  12613  dfuzi  12615  uzind  12616  uzind3  12618  eluz1  12787  uzind4  12851  nnwos  12860  eqreznegel  12879  zmin  12889  elixx1  13302  elioo2  13334  elfz1  13461  flval3  13769  serge0  14013  expge0  14055  expge1  14056  hashbclem  14409  pr2pwpr  14436  elss2prb  14445  hash2sspr  14446  wrdmap  14503  wwlktovfo  14915  shftf  15036  rlimrege0  15536  incexc2  15798  dvdsdivcl  16280  divalglem4  16360  divalgmod  16370  bitsval  16388  bezout  16507  dfgcd2  16510  lcmledvds  16563  lcmgcdlem  16570  lcmfledvds  16596  1nprm  16643  1idssfct  16644  isprm2  16646  hashdvds  16740  phisum  16756  odzval  16757  odzcllem  16758  odzdvds  16761  prmreclem2  16883  prmreclem5  16886  rami  16981  ramub1lem1  16992  ramub1lem2  16993  prmgaplem3  17019  prmgaplem4  17020  prmgaplem5  17021  prmgaplem6  17022  ismre  17547  ismri  17592  isacs  17612  isacs1i  17618  catlid  17644  catrid  17645  ismon  17695  isnat  17912  eldmcoa  18027  fncnvimaeqv  18081  lubeldm  18312  glbeldm  18325  gsumval2  18649  ismgmhm  18659  issubmgm  18665  rabsubmgmd  18667  mgmhmeql  18679  ismhm  18748  issubm  18766  issubmd  18769  mndind  18791  grplinv  18960  issubg  19097  isnsg  19125  cycsubg  19178  isgim  19232  isga  19261  elcntz  19292  elcntzsn  19295  symgfix2  19386  symgsssg  19437  symgfisg  19438  psgnunilem5  19464  odid  19508  odlem2  19509  gexid  19551  gexlem2  19552  gexdvds  19554  isslw  19578  pgpssslw  19584  pj1id  19669  oddvdssubg  19825  pgpfac1lem5  20051  ablfaclem2  20058  isirred  20394  isrnghm  20416  isrngim  20420  isrim0  20457  issubrng  20523  issubrg  20547  rgspnmin  20591  issdrg  20764  isabv  20787  islss  20928  islmhm  21021  islmim  21056  islbs  21070  psgndiflemB  21579  elocv  21647  isobs  21699  dsmmelbas  21718  frlmelbas  21735  islinds  21788  gsumbagdiaglem  21910  rhmpsrlem2  21920  psrlidm  21940  psrridm  21941  psrass1  21942  psrcom  21946  mplsubglem  21977  mpllsslem  21978  evlsval2  22067  ismhp  22132  ismhp3  22134  mhpmulcl  22141  psdmul  22158  coe1ae0  22205  coe1mul2  22259  dmatel  22480  scmatel  22492  scmateALT  22499  symgmatr01lem  22640  pmatcoe1fsupp  22688  cpmatel  22698  chpscmat  22829  istopon  22899  fctop  22991  cctop  22993  ppttop  22994  pptbas  22995  epttop  22996  iscld  23014  clscld  23034  isnei  23090  neips  23100  neiptopnei  23119  iscn  23222  iscnp  23224  cmpsublem  23386  conncompconn  23419  2ndc1stc  23438  2ndcdisj  23443  elkgen  23523  xkoccn  23606  txdis1cn  23622  txkgen  23639  xkococnlem  23646  xkococn  23647  xkoinjcn  23674  txconn  23676  elqtop  23684  elmptrab  23814  fbssfi  23824  opnfbas  23829  elfg  23858  cfinfil  23880  csdfil  23881  supfil  23882  filssufilg  23898  uffix  23908  fixufil  23909  uffixfr  23910  elflim2  23951  fclscf  24012  flimfnfcls  24015  alexsubALTlem2  24035  alexsubALTlem4  24037  alexsubALT  24038  ptcmplem2  24040  elutop  24220  isucn  24264  iscfilu  24274  ispsmet  24291  ismet  24310  isxmet  24311  elblps  24374  elbl  24375  restmetu  24557  icccmp  24813  elcncf  24878  ishtpy  24961  isphtpy  24970  om1elbas  25021  iscfil  25254  iscau  25265  iscmet  25273  lmle  25290  rrxfsupp  25391  minveclem3  25418  minveclem4  25421  ovolshftlem1  25498  ovolscalem1  25502  ovolicc2lem3  25508  dyadmax  25587  dyadmbllem  25588  opnmbllem  25590  vitalilem2  25598  vitalilem3  25599  elcpn  25923  ig1pval3  26165  coelem  26213  quotlem  26288  elqaalem1  26307  elqaalem3  26309  aannenlem1  26316  aannenlem2  26317  dmarea  26943  jensen  26974  ftalem4  27061  efnnfsumcl  27088  efchtdvds  27144  sqff1o  27167  fsumdvdsdiaglem  27168  dvdsppwf1o  27171  dvdsflf1o  27172  dvdsflsumcom  27173  musum  27176  muinv  27178  logfac2  27202  dchrelbas  27221  lgsfle1  27291  lgsle1  27297  lgsdirprm  27316  lgsne0  27320  lgsquadlem1  27365  lgsquadlem2  27366  dchrvmasumlem1  27480  logsqvma  27527  pntleml  27596  ltsval2  27642  ltsres  27648  conway  27793  cutcuts  27795  cutbday  27798  cutsun12  27804  cutbdaybnd2  27810  cutbdaylt  27812  bday1  27828  cutlt  27946  precsexlem8  28228  precsexlem9  28229  precsexlem11  28231  oncutlt  28278  noseqinds  28307  peano5uzs  28418  uzsind  28419  tgellng  28643  mircgr  28747  mirbtwn  28748  iseqlg  28957  ttgelitv  28973  upgrle  29181  upgrbi  29184  umgredg2  29191  umgrbi  29192  edgupgr  29225  edgumgr  29226  upgredg  29228  numedglnl  29235  edgusgr  29251  usgruspgrb  29274  usgredg2ALT  29284  ushgredgedg  29320  ushgredgedgloop  29322  usgrexmplef  29350  upgrreslem  29395  umgrreslem  29396  upgrres1  29404  nbgrel  29431  nbupgrel  29436  nbumgrvtx  29437  nbusgreledg  29444  nbgrnself  29450  uvtxusgrel  29494  vtxdgoddnumeven  29644  rgrusgrprc  29680  lfgrwlkprop  29776  iswwlks  29926  iswwlksn  29928  wwlksnextsurj  29990  rusgrnumwwlkslem  30062  rusgrnumwwlks  30067  isclwwlk  30076  clwwlknscsh  30154  eleclclwwlkn  30168  clwlknf1oclwwlkn  30176  clwwlkvbij  30205  eupth2lems  30330  konigsberglem4  30347  fusgreg2wsplem  30425  2clwwlkel  30441  extwwlkfabel  30445  clwwlknonclwlknonf1o  30454  dlwwlknondlwlknonf1o  30457  numclwwlk2lem1  30468  numclwlk2lem2f  30469  numclwlk2lem2f1o  30471  grpoidinv2  30608  grpoinv  30618  isssp  30817  islno  30846  isblo  30875  ishmo  30904  ubthlem1  30963  ubthlem2  30964  htthlem  31010  ocel  31374  shsval2i  31480  ococin  31501  chsupsn  31506  eleigvec  32050  cnlnadjlem5  32164  shatomistici  32454  hatomistici  32455  dmrab  32588  elrabrd  32590  nnindf  32916  indf1ofs  32949  ismnt  33066  pwrssmgc  33083  tocycf  33202  tocyc01  33203  trsp2cyc  33208  cycpmco2f1  33209  cycpmco2rn  33210  cycpmco2lem2  33212  cycpmco2lem3  33213  cycpmco2lem5  33215  cycpmco2lem6  33216  cycpmco2lem7  33217  cycpmconjv  33227  tocyccntz  33229  cyc3evpm  33235  cycpmgcl  33238  cycpmconjslem2  33240  cyc3conja  33242  isfxp  33253  fxpgaeq  33254  elrgspnsubrun  33334  fldgensdrg  33402  nsgmgclem  33498  nsgmgc  33499  nsgqusf1olem2  33501  isprmidl  33525  ismxidl  33549  ssmxidl  33561  isrprm  33612  1arithufdlem3  33641  1arithufdlem4  33642  1arithufd  33643  mplvrpmlem  33739  mplvrpmga  33741  mplvrpmmhm  33742  fedgmullem2  33826  ply1annnr  33899  minplyann  33905  minplyirred  33907  constrsuc  33934  zarclsiin  34067  zart0  34075  rhmpreimacnlem  34080  ordtconnlem1  34120  sigagenval  34336  ldsysgenld  34356  ldgenpisyslem1  34359  ldgenpisyslem2  34360  ldgenpisys  34362  ddemeas  34432  ismbfm  34447  imambfm  34458  dya2iocuni  34479  oms0  34493  omssubadd  34496  elcarsg  34501  issibf  34529  sitgfval  34537  oddpwdc  34550  eulerpartlemgh  34574  eulerpartlemgs2  34576  dstfrvel  34670  ballotlemfc0  34689  ballotlemfcc  34690  ballotlemiex  34698  ballotlemfrcn0  34726  ballotlemirc  34728  ballotlem7  34732  reprsum  34809  reprsuc  34811  reprpmtf1o  34822  reprdifc  34823  fnrelpredd  35287  fineqvnttrclselem2  35318  connpconn  35478  iscvm  35502  cvmsi  35508  cvmsval  35509  cvmliftmolem2  35525  cvmliftiota  35544  snmlval  35574  satfv1lem  35605  fmlafvel  35628  fmla1  35630  fmlaomn0  35633  satfv0fvfmla0  35656  sategoelfvb  35662  elmpst  35779  lineelsb2  36391  linerflx1  36392  fwddifval  36405  fwddifnval  36406  rankeq1o  36414  finminlem  36561  fneint  36591  fnessref  36600  topmeet  36607  topjoin  36608  neifg  36614  weiunlem  36706  weiunfrlem  36707  weiunse  36711  regsfromregtco  36781  relowlssretop  37740  fin2solem  37988  fin2so  37989  poimirlem4  38006  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  poimirlem31  38033  poimirlem32  38034  opnmbllem0  38038  mblfinlem2  38040  itg2gt0cn  38057  indexa  38115  nninfnub  38133  istotbnd  38151  sstotbnd2  38156  isbnd  38162  isrngohom  38347  isrngoiso  38360  isidl  38396  ispridl  38416  ismaxidl  38422  prnc  38449  isfldidl  38450  islshp  39486  lssats  39519  islfl  39567  isat  39793  atlatmstc  39826  islln  40013  islpln  40037  islvol  40080  linepsubN  40259  elpmap  40265  pmapsub  40275  elpadd  40306  paddvaln0N  40308  islhp  40503  isldil  40617  isltrn  40626  isdilN  40661  istrnN  40664  diaval  41539  diaelval  41540  diaeldm  41543  diaelrnN  41552  cdlemm10N  41625  docaclN  41631  dibglbN  41673  dicval  41683  dicfnN  41690  dicvalrelN  41692  dihglblem2aN  41800  dihglblem2N  41801  dihglblem3N  41802  dih1dimatlem  41836  dihglb2  41849  dochvalr  41864  doch2val2  41871  dochocss  41873  islpolN  41990  mapd0  42172  aks4d1p4  42579  aks4d1p7  42583  isprimroot  42593  linvh  42596  primrootsunit1  42597  primrootscoprmpow  42599  primrootscoprbij  42602  sticksstones3  42648  aks6d1c6lem3  42672  grpods  42694  unitscyglem2  42696  unitscyglem4  42698  unitscyglem5  42699  supinf  42741  fsuppssindlem2  43057  infdesc  43108  isnacs  43168  elmzpcl  43190  mzpindd  43210  rencldnfilem  43280  irrapxlem6  43287  pellexlem3  43291  pellexlem5  43293  elpell1qr  43307  elpell14qr  43309  elpell1234qr  43311  pellfundre  43341  pellfundge  43342  pellfundlb  43344  pellfundglb  43345  rmspecnonsq  43367  jm2.22  43455  jm2.23  43456  rpnnen3lem  43491  fnwe2lem2  43511  elmnc  43596  dgraalem  43605  dgraaub  43608  mpaalem  43612  onsucelab  43723  limnsuc  43725  sqrtcvallem1  44090  rfovcnvf1od  44463  scottelrankd  44706  nzss  44776  iccshift  45977  iooshift  45981  limcperiod  46087  sumnnodd  46089  ioodvbdlimc1lem1  46388  dvnprodlem1  46403  dvnprodlem3  46405  itgperiod  46438  stoweidlem14  46471  stoweidlem15  46472  stoweidlem16  46473  stoweidlem31  46488  stoweidlem36  46493  stoweidlem46  46503  stoweidlem48  46505  fourierdlem2  46566  fourierdlem3  46567  fourierdlem20  46584  fourierdlem25  46589  fourierdlem37  46601  fourierdlem42  46606  fourierdlem48  46611  fourierdlem51  46614  fourierdlem63  46626  fourierdlem64  46627  fourierdlem65  46628  fourierdlem79  46642  fourierdlem81  46644  elaa2lem  46690  etransclem24  46715  etransclem26  46717  etransclem28  46719  etransclem35  46726  etransclem48  46739  salgenval  46778  salgenn0  46788  salgencl  46789  sssalgen  46792  salgenss  46793  salgenuni  46794  issalgend  46795  salgencntex  46800  subsaliuncllem  46814  sge0fodjrnlem  46873  meadjiunlem  46922  caragenel  46952  ovnlecvr  47015  ovnpnfelsup  47016  ovncvrrp  47021  ovnsubaddlem1  47027  hoidmv1lelem1  47048  hoidmv1lelem2  47049  hoidmv1lelem3  47050  hoidmvlelem1  47052  hoidmvlelem2  47053  hoidmvlelem4  47055  ovnhoilem1  47058  ovnlecvr2  47067  ovncvr2  47068  issmflem  47184  smflimlem2  47229  smflimlem3  47230  smflimsuplem2  47278  elsetpreimafvrab  47883  iccpart  47905  sprel  47973  prelspr  47975  sprsymrelfolem2  47982  sprsymrelf  47984  prpair  47990  paireqne  48000  prprelb  48005  prprelprb  48006  dfodd2  48141  dfeven5  48171  dfodd7  48172  fpprel  48233  clnbgrel  48333  clnbupgrel  48339  sclnbgrel  48352  vopnbgrel  48359  dfclnbgr6  48361  dfnbgr6  48362  isubgredg  48371  uhgrimisgrgric  48436  grtriprop  48446  isgrtri  48448  stgredgel  48462  stgrusgra  48464  uspgrlimlem3  48495  uspgrlim  48497  grlimgredgex  48505  grlimgrtrilem2  48507  gpgiedgdmel  48554  gpgedgel  48555  gpgnbgrvtx0  48579  gpgnbgrvtx1  48580  gpgprismgr4cycllem10  48609  1hegrlfgr  48637  assintop  48714  isassintop  48715  assintopcllaw  48717  0even  48742  2even  48744  2zrngamgm  48750  dmatALTbasel  48907  lcoval  48917  elbigo  49056  elrrx2linest2  49250  itsclc0  49276  itsclc0b  49277  itscnhlinecirc02p  49290  unilbss  49322  secval  50251  cscval  50252  cotval  50253