Theorem elrab 3684

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 3493	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3493	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 482	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2822	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3434	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3671	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 380	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3433  Vcvv 3475

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477

This theorem is referenced by:  elrab3  3685  elrabd  3686  elrab2  3687  ralrab  3690  rexrab  3693  reurab  3698  rabsnt  4736  unimax  4949  ssintub  4971  intminss  4979  rabxfrd  5416  ssimaex  6977  weniso  7351  canth  7362  riotarab  7408  sorpsscmpl  7724  onnminsb  7787  dfom2  7857  ssnlim  7875  elsuppfng  8155  elsuppfn  8156  ressuppssdif  8170  oeeulem  8601  cofonr  8673  elpmg  8837  fineqvlem  9262  mapfienlem2  9401  supub  9454  suplub  9455  ordtypelem6  9518  ordtypelem7  9519  hartogslem1  9537  hartogs  9539  wemapsolem  9545  card2on  9549  elharval  9556  wdom2d  9575  cantnfs  9661  scottex  9880  tskwe  9945  cardid2  9948  iscard2  9971  cardmin2  9994  acni3  10042  alephsuc2  10075  kmlem1  10145  cofsmo  10264  coftr  10268  fin23lem11  10312  enfin2i  10316  fin1a2lem9  10403  fin1a2lem11  10405  axcc4  10434  axdc3lem2  10446  zorn2lem7  10497  ondomon  10558  alephval2  10567  grutsk  10817  negf1o  11644  infm3  12173  nnind  12230  peano2uz2  12650  peano5uzi  12651  dfuzi  12653  uzind  12654  uzind3  12656  eluz1  12826  uzind4  12890  nnwos  12899  eqreznegel  12918  zmin  12928  elixx1  13333  elioo2  13365  elfz1  13489  flval3  13780  serge0  14022  expge0  14064  expge1  14065  hashbclem  14411  pr2pwpr  14440  elss2prb  14448  hash2sspr  14449  wrdmap  14496  wwlktovfo  14909  shftf  15026  rlimrege0  15523  incexc2  15784  dvdsdivcl  16259  divalglem4  16339  divalgmod  16349  bitsval  16365  bezout  16485  dfgcd2  16488  lcmledvds  16536  lcmgcdlem  16543  lcmfledvds  16569  1nprm  16616  1idssfct  16617  isprm2  16619  hashdvds  16708  phisum  16723  odzval  16724  odzcllem  16725  odzdvds  16728  prmreclem2  16850  prmreclem5  16853  rami  16948  ramub1lem1  16959  ramub1lem2  16960  prmgaplem3  16986  prmgaplem4  16987  prmgaplem5  16988  prmgaplem6  16989  ismre  17534  ismri  17575  isacs  17595  isacs1i  17601  catlid  17627  catrid  17628  ismon  17680  isnat  17898  eldmcoa  18015  fncnvimaeqv  18071  lubeldm  18306  glbeldm  18319  gsumval2  18605  ismhm  18673  issubm  18684  issubmd  18687  mndind  18709  grplinv  18874  issubg  19006  isnsg  19035  cycsubg  19085  isgim  19136  isga  19155  elcntz  19186  elcntzsn  19189  symgfix2  19284  symgsssg  19335  symgfisg  19336  psgnunilem5  19362  odid  19406  odlem2  19407  gexid  19449  gexlem2  19450  gexdvds  19452  isslw  19476  pgpssslw  19482  pj1id  19567  oddvdssubg  19723  pgpfac1lem5  19949  ablfaclem2  19956  isirred  20233  isrim0OLD  20259  isrim0  20261  issubrg  20319  issdrg  20404  isabv  20427  islss  20545  islmhm  20638  islmim  20673  islbs  20687  psgndiflemB  21153  elocv  21221  isobs  21275  dsmmelbas  21294  frlmelbas  21311  islinds  21364  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  psrmulcllem  21506  psrlidm  21523  psrridm  21524  psrass1  21525  psrcom  21529  mplsubglem  21558  mpllsslem  21559  evlsval2  21650  ismhp  21684  ismhp3  21686  mhpmulcl  21692  coe1ae0  21740  coe1mul2  21791  dmatel  21995  scmatel  22007  scmateALT  22014  symgmatr01lem  22155  pmatcoe1fsupp  22203  cpmatel  22213  chpscmat  22344  istopon  22414  fctop  22507  cctop  22509  ppttop  22510  pptbas  22511  epttop  22512  iscld  22531  clscld  22551  isnei  22607  neips  22617  neiptopnei  22636  iscn  22739  iscnp  22741  cmpsublem  22903  conncompconn  22936  2ndc1stc  22955  2ndcdisj  22960  elkgen  23040  xkoccn  23123  txdis1cn  23139  txkgen  23156  xkococnlem  23163  xkococn  23164  xkoinjcn  23191  txconn  23193  elqtop  23201  elmptrab  23331  fbssfi  23341  opnfbas  23346  elfg  23375  cfinfil  23397  csdfil  23398  supfil  23399  filssufilg  23415  uffix  23425  fixufil  23426  uffixfr  23427  elflim2  23468  fclscf  23529  flimfnfcls  23532  alexsubALTlem2  23552  alexsubALTlem4  23554  alexsubALT  23555  ptcmplem2  23557  elutop  23738  isucn  23783  iscfilu  23793  ispsmet  23810  ismet  23829  isxmet  23830  elblps  23893  elbl  23894  restmetu  24079  icccmp  24341  elcncf  24405  ishtpy  24488  isphtpy  24497  om1elbas  24548  iscfil  24782  iscau  24793  iscmet  24801  lmle  24818  rrxfsupp  24919  minveclem3  24946  minveclem4  24949  ovolshftlem1  25026  ovolscalem1  25030  ovolicc2lem3  25036  dyadmax  25115  dyadmbllem  25116  opnmbllem  25118  vitalilem2  25126  vitalilem3  25127  elcpn  25451  ig1pval3  25692  coelem  25740  quotlem  25813  elqaalem1  25832  elqaalem3  25834  aannenlem1  25841  aannenlem2  25842  dmarea  26462  jensen  26493  ftalem4  26580  efnnfsumcl  26607  efchtdvds  26663  sqff1o  26686  fsumdvdsdiaglem  26687  dvdsppwf1o  26690  dvdsflf1o  26691  dvdsflsumcom  26692  musum  26695  muinv  26697  logfac2  26720  dchrelbas  26739  lgsfle1  26809  lgsle1  26815  lgsdirprm  26834  lgsne0  26838  lgsquadlem1  26883  lgsquadlem2  26884  dchrvmasumlem1  26998  logsqvma  27045  pntleml  27114  sltval2  27159  sltres  27165  conway  27300  scutcut  27302  scutbday  27305  scutun12  27311  scutbdaybnd2  27317  scutbdaylt  27319  bday1s  27332  cutlt  27419  precsexlem8  27660  precsexlem9  27661  precsexlem11  27663  tgellng  27804  mircgr  27908  mirbtwn  27909  iseqlg  28118  ttgelitv  28140  upgrle  28350  upgrbi  28353  umgredg2  28360  umgrbi  28361  edgupgr  28394  edgumgr  28395  upgredg  28397  numedglnl  28404  edgusgr  28420  usgruspgrb  28441  usgredg2ALT  28450  ushgredgedg  28486  ushgredgedgloop  28488  usgrexmplef  28516  upgrreslem  28561  umgrreslem  28562  upgrres1  28570  nbgrel  28597  nbupgrel  28602  nbumgrvtx  28603  nbusgreledg  28610  nbgrnself  28616  uvtxusgrel  28660  vtxdgoddnumeven  28810  rgrusgrprc  28846  lfgrwlkprop  28944  iswwlks  29090  iswwlksn  29092  wwlksnextsurj  29154  rusgrnumwwlkslem  29223  rusgrnumwwlks  29228  isclwwlk  29237  clwwlknscsh  29315  eleclclwwlkn  29329  clwlknf1oclwwlkn  29337  clwwlkvbij  29366  eupth2lems  29491  konigsberglem4  29508  fusgreg2wsplem  29586  2clwwlkel  29602  extwwlkfabel  29606  clwwlknonclwlknonf1o  29615  dlwwlknondlwlknonf1o  29618  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  grpoidinv2  29768  grpoinv  29778  isssp  29977  islno  30006  isblo  30035  ishmo  30064  ubthlem1  30123  ubthlem2  30124  htthlem  30170  ocel  30534  shsval2i  30640  ococin  30661  chsupsn  30666  eleigvec  31210  cnlnadjlem5  31324  shatomistici  31614  hatomistici  31615  dmrab  31737  nnindf  32025  ismnt  32153  pwrssmgc  32170  tocycf  32276  tocyc01  32277  trsp2cyc  32282  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmconjv  32301  tocyccntz  32303  cyc3evpm  32309  cycpmgcl  32312  cycpmconjslem2  32314  cyc3conja  32316  fldgensdrg  32404  nsgmgclem  32522  nsgmgc  32523  nsgqusf1olem2  32525  isprmidl  32556  ismxidl  32578  ssmxidl  32590  isrprm  32634  fedgmullem2  32715  ply1annnr  32764  minplyirred  32770  zarclsiin  32851  zart0  32859  rhmpreimacnlem  32864  ordtconnlem1  32904  indf1ofs  33024  sigagenval  33138  ldsysgenld  33158  ldgenpisyslem1  33161  ldgenpisyslem2  33162  ldgenpisys  33164  ddemeas  33234  ismbfm  33249  imambfm  33261  dya2iocuni  33282  oms0  33296  omssubadd  33299  elcarsg  33304  issibf  33332  sitgfval  33340  oddpwdc  33353  eulerpartlemgh  33377  eulerpartlemgs2  33379  dstfrvel  33472  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  ballotlemfrcn0  33528  ballotlemirc  33530  ballotlem7  33534  reprsum  33625  reprsuc  33627  reprpmtf1o  33638  reprdifc  33639  fnrelpredd  34092  connpconn  34226  iscvm  34250  cvmsi  34256  cvmsval  34257  cvmliftmolem2  34273  cvmliftiota  34292  snmlval  34322  satfv1lem  34353  fmlafvel  34376  fmla1  34378  fmlaomn0  34381  satfv0fvfmla0  34404  sategoelfvb  34410  elmpst  34527  lineelsb2  35120  linerflx1  35121  fwddifval  35134  fwddifnval  35135  rankeq1o  35143  finminlem  35203  fneint  35233  fnessref  35242  topmeet  35249  topjoin  35250  neifg  35256  relowlssretop  36244  fin2solem  36474  fin2so  36475  poimirlem4  36492  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  opnmbllem0  36524  mblfinlem2  36526  itg2gt0cn  36543  indexa  36601  nninfnub  36619  istotbnd  36637  sstotbnd2  36642  isbnd  36648  isrngohom  36833  isrngoiso  36846  isidl  36882  ispridl  36902  ismaxidl  36908  prnc  36935  isfldidl  36936  islshp  37849  lssats  37882  islfl  37930  isat  38156  atlatmstc  38189  islln  38377  islpln  38401  islvol  38444  linepsubN  38623  elpmap  38629  pmapsub  38639  elpadd  38670  paddvaln0N  38672  islhp  38867  isldil  38981  isltrn  38990  isdilN  39025  istrnN  39028  diaval  39903  diaelval  39904  diaeldm  39907  diaelrnN  39916  cdlemm10N  39989  docaclN  39995  dibglbN  40037  dicval  40047  dicfnN  40054  dicvalrelN  40056  dihglblem2aN  40164  dihglblem2N  40165  dihglblem3N  40166  dih1dimatlem  40200  dihglb2  40213  dochvalr  40228  doch2val2  40235  dochocss  40237  islpolN  40354  mapd0  40536  aks4d1p4  40944  aks4d1p7  40948  sticksstones3  40964  rhmmpllem2  41122  rhmcomulmpl  41124  fsuppssindlem2  41164  infdesc  41385  isnacs  41442  elmzpcl  41464  mzpindd  41484  rencldnfilem  41558  irrapxlem6  41565  pellexlem3  41569  pellexlem5  41571  elpell1qr  41585  elpell14qr  41587  elpell1234qr  41589  pellfundre  41619  pellfundge  41620  pellfundlb  41622  pellfundglb  41623  rmspecnonsq  41645  jm2.22  41734  jm2.23  41735  rpnnen3lem  41770  fnwe2lem2  41793  elmnc  41878  dgraalem  41887  dgraaub  41890  mpaalem  41894  rgspnmin  41913  onsucelab  42013  limnsuc  42015  sqrtcvallem1  42382  rfovcnvf1od  42755  scottelrankd  43006  nzss  43076  iccshift  44231  iooshift  44235  limcperiod  44344  sumnnodd  44346  ioodvbdlimc1lem1  44647  dvnprodlem1  44662  dvnprodlem3  44664  itgperiod  44697  stoweidlem14  44730  stoweidlem15  44731  stoweidlem16  44732  stoweidlem31  44747  stoweidlem36  44752  stoweidlem46  44762  stoweidlem48  44764  fourierdlem2  44825  fourierdlem3  44826  fourierdlem20  44843  fourierdlem25  44848  fourierdlem37  44860  fourierdlem42  44865  fourierdlem48  44870  fourierdlem51  44873  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem79  44901  fourierdlem81  44903  elaa2lem  44949  etransclem24  44974  etransclem26  44976  etransclem28  44978  etransclem35  44985  etransclem48  44998  salgenval  45037  salgenn0  45047  salgencl  45048  sssalgen  45051  salgenss  45052  salgenuni  45053  issalgend  45054  salgencntex  45059  subsaliuncllem  45073  sge0fodjrnlem  45132  meadjiunlem  45181  caragenel  45211  ovnlecvr  45274  ovnpnfelsup  45275  ovncvrrp  45280  ovnsubaddlem1  45286  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem4  45314  ovnhoilem1  45317  ovnlecvr2  45326  ovncvr2  45327  issmflem  45443  smflimlem2  45488  smflimlem3  45489  smflimsuplem2  45537  elsetpreimafvrab  46062  iccpart  46084  sprel  46152  prelspr  46154  sprsymrelfolem2  46161  sprsymrelf  46163  prpair  46169  paireqne  46179  prprelb  46184  prprelprb  46185  dfodd2  46304  dfeven5  46334  dfodd7  46335  fpprel  46396  1hegrlfgr  46510  ismgmhm  46553  issubmgm  46559  rabsubmgmd  46561  mgmhmeql  46573  assintop  46619  isassintop  46620  assintopcllaw  46622  isrnghm  46690  isrngisom  46694  issubrng  46726  0even  46829  2even  46831  2zrngamgm  46837  dmatALTbasel  47083  lcoval  47093  elbigo  47237  elrrx2linest2  47431  itsclc0  47457  itsclc0b  47458  itscnhlinecirc02p  47471  unilbss  47502  secval  47792  cscval  47793  cotval  47794