Theorem elrab 3625

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {crab 3069  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435

This theorem is referenced by:  elrab3  3626  elrabd  3627  elrab2  3628  ralrab  3631  rexrab  3634  rabsnt  4668  unimax  4878  ssintub  4898  intminss  4906  rabxfrd  5341  ssimaex  6862  weniso  7234  canth  7238  sorpsscmpl  7596  onnminsb  7658  dfom2  7723  ssnlim  7741  elsuppfng  7995  elsuppfn  7996  ressuppssdif  8010  oeeulem  8441  elpmg  8640  fineqvlem  9046  mapfienlem2  9174  supub  9227  suplub  9228  ordtypelem6  9291  ordtypelem7  9292  hartogslem1  9310  hartogs  9312  wemapsolem  9318  card2on  9322  elharval  9329  wdom2d  9348  cantnfs  9433  scottex  9652  tskwe  9717  cardid2  9720  iscard2  9743  cardmin2  9766  acni3  9812  alephsuc2  9845  kmlem1  9915  cofsmo  10034  coftr  10038  fin23lem11  10082  enfin2i  10086  fin1a2lem9  10173  fin1a2lem11  10175  axcc4  10204  axdc3lem2  10216  zorn2lem7  10267  ondomon  10328  alephval2  10337  grutsk  10587  negf1o  11414  infm3  11943  nnind  12000  peano2uz2  12417  peano5uzi  12418  dfuzi  12420  uzind  12421  uzind3  12423  eluz1  12595  uzind4  12655  nnwos  12664  eqreznegel  12683  zmin  12693  elixx1  13097  elioo2  13129  elfz1  13253  flval3  13544  serge0  13786  expge0  13828  expge1  13829  hashbclem  14173  pr2pwpr  14202  elss2prb  14210  hash2sspr  14211  wrdmap  14258  wwlktovfo  14682  shftf  14799  rlimrege0  15297  incexc2  15559  dvdsdivcl  16034  divalglem4  16114  divalgmod  16124  bitsval  16140  bezout  16260  dfgcd2  16263  lcmledvds  16313  lcmgcdlem  16320  lcmfledvds  16346  1nprm  16393  1idssfct  16394  isprm2  16396  hashdvds  16485  phisum  16500  odzval  16501  odzcllem  16502  odzdvds  16505  prmreclem2  16627  prmreclem5  16630  rami  16725  ramub1lem1  16736  ramub1lem2  16737  prmgaplem3  16763  prmgaplem4  16764  prmgaplem5  16765  prmgaplem6  16766  ismre  17308  ismri  17349  isacs  17369  isacs1i  17375  catlid  17401  catrid  17402  ismon  17454  isnat  17672  eldmcoa  17789  fncnvimaeqv  17845  lubeldm  18080  glbeldm  18093  gsumval2  18379  ismhm  18441  issubm  18451  issubmd  18454  mndind  18475  grplinv  18637  issubg  18764  isnsg  18792  cycsubg  18836  isgim  18887  isga  18906  elcntz  18937  elcntzsn  18940  symgfix2  19033  symgsssg  19084  symgfisg  19085  psgnunilem5  19111  odid  19155  odlem2  19156  gexid  19195  gexlem2  19196  gexdvds  19198  isslw  19222  pgpssslw  19228  pj1id  19314  oddvdssubg  19465  pgpfac1lem5  19691  ablfaclem2  19698  isirred  19950  isrim0  19976  issubrg  20033  issdrg  20072  isabv  20088  islss  20205  islmhm  20298  islmim  20333  islbs  20347  psgndiflemB  20814  elocv  20882  isobs  20936  dsmmelbas  20955  frlmelbas  20972  islinds  21025  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  psrmulcllem  21165  psrlidm  21181  psrridm  21182  psrass1  21183  psrcom  21187  mplsubglem  21214  mpllsslem  21215  evlsval2  21306  ismhp  21340  ismhp3  21342  mhpmulcl  21348  coe1ae0  21396  coe1mul2  21449  dmatel  21651  scmatel  21663  scmateALT  21670  symgmatr01lem  21811  pmatcoe1fsupp  21859  cpmatel  21869  chpscmat  22000  istopon  22070  fctop  22163  cctop  22165  ppttop  22166  pptbas  22167  epttop  22168  iscld  22187  clscld  22207  isnei  22263  neips  22273  neiptopnei  22292  iscn  22395  iscnp  22397  cmpsublem  22559  conncompconn  22592  2ndc1stc  22611  2ndcdisj  22616  elkgen  22696  xkoccn  22779  txdis1cn  22795  txkgen  22812  xkococnlem  22819  xkococn  22820  xkoinjcn  22847  txconn  22849  elqtop  22857  elmptrab  22987  fbssfi  22997  opnfbas  23002  elfg  23031  cfinfil  23053  csdfil  23054  supfil  23055  filssufilg  23071  uffix  23081  fixufil  23082  uffixfr  23083  elflim2  23124  fclscf  23185  flimfnfcls  23188  alexsubALTlem2  23208  alexsubALTlem4  23210  alexsubALT  23211  ptcmplem2  23213  elutop  23394  isucn  23439  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  elblps  23549  elbl  23550  restmetu  23735  icccmp  23997  elcncf  24061  ishtpy  24144  isphtpy  24153  om1elbas  24204  iscfil  24438  iscau  24449  iscmet  24457  lmle  24474  rrxfsupp  24575  minveclem3  24602  minveclem4  24605  ovolshftlem1  24682  ovolscalem1  24686  ovolicc2lem3  24692  dyadmax  24771  dyadmbllem  24772  opnmbllem  24774  vitalilem2  24782  vitalilem3  24783  elcpn  25107  ig1pval3  25348  coelem  25396  quotlem  25469  elqaalem1  25488  elqaalem3  25490  aannenlem1  25497  aannenlem2  25498  dmarea  26116  jensen  26147  ftalem4  26234  efnnfsumcl  26261  efchtdvds  26317  sqff1o  26340  fsumdvdsdiaglem  26341  dvdsppwf1o  26344  dvdsflf1o  26345  dvdsflsumcom  26346  musum  26349  muinv  26351  logfac2  26374  dchrelbas  26393  lgsfle1  26463  lgsle1  26469  lgsdirprm  26488  lgsne0  26492  lgsquadlem1  26537  lgsquadlem2  26538  dchrvmasumlem1  26652  logsqvma  26699  pntleml  26768  tgellng  26923  mircgr  27027  mirbtwn  27028  iseqlg  27237  ttgelitv  27259  upgrle  27469  upgrbi  27472  umgredg2  27479  umgrbi  27480  edgupgr  27513  edgumgr  27514  upgredg  27516  numedglnl  27523  edgusgr  27539  usgruspgrb  27560  usgredg2ALT  27569  ushgredgedg  27605  ushgredgedgloop  27607  usgrexmplef  27635  upgrreslem  27680  umgrreslem  27681  upgrres1  27689  nbgrel  27716  nbupgrel  27721  nbumgrvtx  27722  nbusgreledg  27729  nbgrnself  27735  uvtxusgrel  27779  vtxdgoddnumeven  27929  rgrusgrprc  27965  lfgrwlkprop  28064  iswwlks  28210  iswwlksn  28212  wwlksnextsurj  28274  rusgrnumwwlkslem  28343  rusgrnumwwlks  28348  isclwwlk  28357  clwwlknscsh  28435  eleclclwwlkn  28449  clwlknf1oclwwlkn  28457  clwwlkvbij  28486  eupth2lems  28611  konigsberglem4  28628  fusgreg2wsplem  28706  2clwwlkel  28722  extwwlkfabel  28726  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1o  28738  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  grpoidinv2  28886  grpoinv  28896  isssp  29095  islno  29124  isblo  29153  ishmo  29182  ubthlem1  29241  ubthlem2  29242  htthlem  29288  ocel  29652  shsval2i  29758  ococin  29779  chsupsn  29784  eleigvec  30328  cnlnadjlem5  30442  shatomistici  30732  hatomistici  30733  dmrab  30853  nnindf  31142  ismnt  31270  pwrssmgc  31287  tocycf  31393  tocyc01  31394  trsp2cyc  31399  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmconjv  31418  tocyccntz  31420  cyc3evpm  31426  cycpmgcl  31429  cycpmconjslem2  31431  cyc3conja  31433  nsgmgclem  31605  nsgmgc  31606  nsgqusf1olem2  31608  isprmidl  31622  ismxidl  31643  ssmxidl  31651  isrprm  31674  fedgmullem2  31720  zarclsiin  31830  zart0  31838  rhmpreimacnlem  31843  ordtconnlem1  31883  indf1ofs  32003  sigagenval  32117  ldsysgenld  32137  ldgenpisyslem1  32140  ldgenpisyslem2  32141  ldgenpisys  32143  ddemeas  32213  ismbfm  32228  imambfm  32238  dya2iocuni  32259  oms0  32273  omssubadd  32276  elcarsg  32281  issibf  32309  sitgfval  32317  oddpwdc  32330  eulerpartlemgh  32354  eulerpartlemgs2  32356  dstfrvel  32449  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemiex  32477  ballotlemfrcn0  32505  ballotlemirc  32507  ballotlem7  32511  reprsum  32602  reprsuc  32604  reprpmtf1o  32615  reprdifc  32616  fnrelpredd  33070  connpconn  33206  iscvm  33230  cvmsi  33236  cvmsval  33237  cvmliftmolem2  33253  cvmliftiota  33272  snmlval  33302  satfv1lem  33333  fmlafvel  33356  fmla1  33358  fmlaomn0  33361  satfv0fvfmla0  33384  sategoelfvb  33390  elmpst  33507  riotarab  33682  reurab  33683  sltval2  33868  sltres  33874  conway  34002  scutcut  34004  scutbday  34007  scutun12  34013  scutbdaybnd2  34019  scutbdaylt  34021  bday1s  34034  lineelsb2  34459  linerflx1  34460  fwddifval  34473  fwddifnval  34474  rankeq1o  34482  finminlem  34516  fneint  34546  fnessref  34555  topmeet  34562  topjoin  34563  neifg  34569  relowlssretop  35543  fin2solem  35772  fin2so  35773  poimirlem4  35790  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  poimirlem32  35818  opnmbllem0  35822  mblfinlem2  35824  itg2gt0cn  35841  indexa  35900  nninfnub  35918  istotbnd  35936  sstotbnd2  35941  isbnd  35947  isrngohom  36132  isrngoiso  36145  isidl  36181  ispridl  36201  ismaxidl  36207  prnc  36234  isfldidl  36235  islshp  37000  lssats  37033  islfl  37081  isat  37307  atlatmstc  37340  islln  37527  islpln  37551  islvol  37594  linepsubN  37773  elpmap  37779  pmapsub  37789  elpadd  37820  paddvaln0N  37822  islhp  38017  isldil  38131  isltrn  38140  isdilN  38175  istrnN  38178  diaval  39053  diaelval  39054  diaeldm  39057  diaelrnN  39066  cdlemm10N  39139  docaclN  39145  dibglbN  39187  dicval  39197  dicfnN  39204  dicvalrelN  39206  dihglblem2aN  39314  dihglblem2N  39315  dihglblem3N  39316  dih1dimatlem  39350  dihglb2  39363  dochvalr  39378  doch2val2  39385  dochocss  39387  islpolN  39504  mapd0  39686  aks4d1p4  40094  aks4d1p7  40098  sticksstones3  40111  fsuppssindlem2  40288  infdesc  40487  isnacs  40533  elmzpcl  40555  mzpindd  40575  rencldnfilem  40649  irrapxlem6  40656  pellexlem3  40660  pellexlem5  40662  elpell1qr  40676  elpell14qr  40678  elpell1234qr  40680  pellfundre  40710  pellfundge  40711  pellfundlb  40713  pellfundglb  40714  rmspecnonsq  40736  jm2.22  40824  jm2.23  40825  rpnnen3lem  40860  fnwe2lem2  40883  elmnc  40968  dgraalem  40977  dgraaub  40980  mpaalem  40984  rgspnmin  41003  sqrtcvallem1  41246  rfovcnvf1od  41619  scottelrankd  41872  nzss  41942  iccshift  43063  iooshift  43067  limcperiod  43176  sumnnodd  43178  ioodvbdlimc1lem1  43479  dvnprodlem1  43494  dvnprodlem3  43496  itgperiod  43529  stoweidlem14  43562  stoweidlem15  43563  stoweidlem16  43564  stoweidlem31  43579  stoweidlem36  43584  stoweidlem46  43594  stoweidlem48  43596  fourierdlem2  43657  fourierdlem3  43658  fourierdlem20  43675  fourierdlem25  43680  fourierdlem37  43692  fourierdlem42  43697  fourierdlem48  43702  fourierdlem51  43705  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem79  43733  fourierdlem81  43735  elaa2lem  43781  etransclem24  43806  etransclem26  43808  etransclem28  43810  etransclem35  43817  etransclem48  43830  salgenval  43869  salgenn0  43877  salgencl  43878  sssalgen  43881  salgenss  43882  salgenuni  43883  issalgend  43884  salgencntex  43889  subsaliuncllem  43903  sge0fodjrnlem  43961  meadjiunlem  44010  caragenel  44040  ovnlecvr  44103  ovnpnfelsup  44104  ovncvrrp  44109  ovnsubaddlem1  44115  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem4  44143  ovnhoilem1  44146  ovnlecvr2  44155  ovncvr2  44156  issmflem  44272  smflimlem2  44317  smflimlem3  44318  smflimsuplem2  44365  elsetpreimafvrab  44857  iccpart  44879  sprel  44947  prelspr  44949  sprsymrelfolem2  44956  sprsymrelf  44958  prpair  44964  paireqne  44974  prprelb  44979  prprelprb  44980  dfodd2  45099  dfeven5  45129  dfodd7  45130  fpprel  45191  1hegrlfgr  45305  ismgmhm  45348  issubmgm  45354  rabsubmgmd  45356  mgmhmeql  45368  assintop  45414  isassintop  45415  assintopcllaw  45417  isrnghm  45461  isrngisom  45465  0even  45500  2even  45502  2zrngamgm  45508  dmatALTbasel  45754  lcoval  45764  elbigo  45908  elrrx2linest2  46102  itsclc0  46128  itsclc0b  46129  itscnhlinecirc02p  46142  unilbss  46174  secval  46460  cscval  46461  cotval  46462