Theorem elrab 3629

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {crab 3391  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433

This theorem is referenced by:  elrab3  3630  elrabd  3631  elrab2  3632  ralrab  3635  rexrab  3637  reurab  3642  rabsnt  4663  unimax  4875  ssintub  4896  intminss  4904  rabxfrd  5346  ssimaex  6912  weniso  7298  canth  7310  riotarab  7355  sorpsscmpl  7677  onnminsb  7742  dfom2  7808  ssnlim  7826  elsuppfng  8109  elsuppfn  8110  ressuppssdif  8125  oeeulem  8527  cofonr  8600  elpmg  8780  fineqvlem  9166  mapfienlem2  9309  supub  9362  suplub  9363  ordtypelem6  9428  ordtypelem7  9429  hartogslem1  9447  hartogs  9449  wemapsolem  9455  card2on  9459  elharval  9466  wdom2d  9485  cantnfs  9578  scottex  9800  tskwe  9865  cardid2  9868  iscard2  9891  cardmin2  9914  acni3  9960  alephsuc2  9993  kmlem1  10064  cofsmo  10182  coftr  10186  fin23lem11  10230  enfin2i  10234  fin1a2lem9  10321  fin1a2lem11  10323  axcc4  10352  axdc3lem2  10364  zorn2lem7  10415  ondomon  10476  alephval2  10486  grutsk  10736  negf1o  11571  infm3  12106  nnind  12183  peano2uz2  12608  peano5uzi  12609  dfuzi  12611  uzind  12612  uzind3  12614  eluz1  12783  uzind4  12847  nnwos  12856  eqreznegel  12875  zmin  12885  elixx1  13298  elioo2  13330  elfz1  13457  flval3  13765  serge0  14009  expge0  14051  expge1  14052  hashbclem  14405  pr2pwpr  14432  elss2prb  14441  hash2sspr  14442  wrdmap  14499  wwlktovfo  14911  shftf  15032  rlimrege0  15532  incexc2  15794  dvdsdivcl  16276  divalglem4  16356  divalgmod  16366  bitsval  16384  bezout  16503  dfgcd2  16506  lcmledvds  16559  lcmgcdlem  16566  lcmfledvds  16592  1nprm  16639  1idssfct  16640  isprm2  16642  hashdvds  16736  phisum  16752  odzval  16753  odzcllem  16754  odzdvds  16757  prmreclem2  16879  prmreclem5  16882  rami  16977  ramub1lem1  16988  ramub1lem2  16989  prmgaplem3  17015  prmgaplem4  17016  prmgaplem5  17017  prmgaplem6  17018  ismre  17543  ismri  17588  isacs  17608  isacs1i  17614  catlid  17640  catrid  17641  ismon  17691  isnat  17908  eldmcoa  18023  fncnvimaeqv  18077  lubeldm  18308  glbeldm  18321  gsumval2  18645  ismgmhm  18655  issubmgm  18661  rabsubmgmd  18663  mgmhmeql  18675  ismhm  18744  issubm  18762  issubmd  18765  mndind  18787  grplinv  18956  issubg  19093  isnsg  19121  cycsubg  19174  isgim  19228  isga  19257  elcntz  19288  elcntzsn  19291  symgfix2  19382  symgsssg  19433  symgfisg  19434  psgnunilem5  19460  odid  19504  odlem2  19505  gexid  19547  gexlem2  19548  gexdvds  19550  isslw  19574  pgpssslw  19580  pj1id  19665  oddvdssubg  19821  pgpfac1lem5  20047  ablfaclem2  20054  isirred  20390  isrnghm  20412  isrngim  20416  isrim0  20453  issubrng  20519  issubrg  20543  rgspnmin  20587  issdrg  20760  isabv  20783  islss  20924  islmhm  21017  islmim  21052  islbs  21066  psgndiflemB  21575  elocv  21643  isobs  21695  dsmmelbas  21714  frlmelbas  21731  islinds  21784  gsumbagdiaglem  21906  rhmpsrlem2  21916  psrlidm  21936  psrridm  21937  psrass1  21938  psrcom  21942  mplsubglem  21973  mpllsslem  21974  evlsval2  22063  ismhp  22128  ismhp3  22130  mhpmulcl  22137  psdmul  22154  coe1ae0  22201  coe1mul2  22255  dmatel  22476  scmatel  22488  scmateALT  22495  symgmatr01lem  22636  pmatcoe1fsupp  22684  cpmatel  22694  chpscmat  22825  istopon  22895  fctop  22987  cctop  22989  ppttop  22990  pptbas  22991  epttop  22992  iscld  23010  clscld  23030  isnei  23086  neips  23096  neiptopnei  23115  iscn  23218  iscnp  23220  cmpsublem  23382  conncompconn  23415  2ndc1stc  23434  2ndcdisj  23439  elkgen  23519  xkoccn  23602  txdis1cn  23618  txkgen  23635  xkococnlem  23642  xkococn  23643  xkoinjcn  23670  txconn  23672  elqtop  23680  elmptrab  23810  fbssfi  23820  opnfbas  23825  elfg  23854  cfinfil  23876  csdfil  23877  supfil  23878  filssufilg  23894  uffix  23904  fixufil  23905  uffixfr  23906  elflim2  23947  fclscf  24008  flimfnfcls  24011  alexsubALTlem2  24031  alexsubALTlem4  24033  alexsubALT  24034  ptcmplem2  24036  elutop  24216  isucn  24260  iscfilu  24270  ispsmet  24287  ismet  24306  isxmet  24307  elblps  24370  elbl  24371  restmetu  24553  icccmp  24809  elcncf  24874  ishtpy  24957  isphtpy  24966  om1elbas  25017  iscfil  25250  iscau  25261  iscmet  25269  lmle  25286  rrxfsupp  25387  minveclem3  25414  minveclem4  25417  ovolshftlem1  25494  ovolscalem1  25498  ovolicc2lem3  25504  dyadmax  25583  dyadmbllem  25584  opnmbllem  25586  vitalilem2  25594  vitalilem3  25595  elcpn  25919  ig1pval3  26161  coelem  26209  quotlem  26284  elqaalem1  26303  elqaalem3  26305  aannenlem1  26312  aannenlem2  26313  dmarea  26939  jensen  26970  ftalem4  27057  efnnfsumcl  27084  efchtdvds  27140  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsppwf1o  27167  dvdsflf1o  27168  dvdsflsumcom  27169  musum  27172  muinv  27174  logfac2  27198  dchrelbas  27217  lgsfle1  27287  lgsle1  27293  lgsdirprm  27312  lgsne0  27316  lgsquadlem1  27361  lgsquadlem2  27362  dchrvmasumlem1  27476  logsqvma  27523  pntleml  27592  ltsval2  27638  ltsres  27644  conway  27789  cutcuts  27791  cutbday  27794  cutsun12  27800  cutbdaybnd2  27806  cutbdaylt  27808  bday1  27824  cutlt  27942  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  oncutlt  28274  noseqinds  28303  peano5uzs  28414  uzsind  28415  tgellng  28639  mircgr  28743  mirbtwn  28744  iseqlg  28953  ttgelitv  28969  upgrle  29177  upgrbi  29180  umgredg2  29187  umgrbi  29188  edgupgr  29221  edgumgr  29222  upgredg  29224  numedglnl  29231  edgusgr  29247  usgruspgrb  29270  usgredg2ALT  29280  ushgredgedg  29316  ushgredgedgloop  29318  usgrexmplef  29346  upgrreslem  29391  umgrreslem  29392  upgrres1  29400  nbgrel  29427  nbupgrel  29432  nbumgrvtx  29433  nbusgreledg  29440  nbgrnself  29446  uvtxusgrel  29490  vtxdgoddnumeven  29640  rgrusgrprc  29676  lfgrwlkprop  29772  iswwlks  29922  iswwlksn  29924  wwlksnextsurj  29986  rusgrnumwwlkslem  30058  rusgrnumwwlks  30063  isclwwlk  30072  clwwlknscsh  30150  eleclclwwlkn  30164  clwlknf1oclwwlkn  30172  clwwlkvbij  30201  eupth2lems  30326  konigsberglem4  30343  fusgreg2wsplem  30421  2clwwlkel  30437  extwwlkfabel  30441  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1o  30453  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  grpoidinv2  30604  grpoinv  30614  isssp  30813  islno  30842  isblo  30871  ishmo  30900  ubthlem1  30959  ubthlem2  30960  htthlem  31006  ocel  31370  shsval2i  31476  ococin  31497  chsupsn  31502  eleigvec  32046  cnlnadjlem5  32160  shatomistici  32450  hatomistici  32451  dmrab  32584  elrabrd  32586  nnindf  32912  indf1ofs  32945  ismnt  33062  pwrssmgc  33079  tocycf  33198  tocyc01  33199  trsp2cyc  33204  cycpmco2f1  33205  cycpmco2rn  33206  cycpmco2lem2  33208  cycpmco2lem3  33209  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmconjv  33223  tocyccntz  33225  cyc3evpm  33231  cycpmgcl  33234  cycpmconjslem2  33236  cyc3conja  33238  isfxp  33249  fxpgaeq  33250  elrgspnsubrun  33330  fldgensdrg  33398  nsgmgclem  33494  nsgmgc  33495  nsgqusf1olem2  33497  isprmidl  33521  ismxidl  33545  ssmxidl  33557  isrprm  33600  1arithufdlem3  33629  1arithufdlem4  33630  1arithufd  33631  mplvrpmlem  33727  mplvrpmga  33729  mplvrpmmhm  33730  fedgmullem2  33814  ply1annnr  33887  minplyann  33893  minplyirred  33895  constrsuc  33922  zarclsiin  34055  zart0  34063  rhmpreimacnlem  34068  ordtconnlem1  34108  sigagenval  34324  ldsysgenld  34344  ldgenpisyslem1  34347  ldgenpisyslem2  34348  ldgenpisys  34350  ddemeas  34420  ismbfm  34435  imambfm  34446  dya2iocuni  34467  oms0  34481  omssubadd  34484  elcarsg  34489  issibf  34517  sitgfval  34525  oddpwdc  34538  eulerpartlemgh  34562  eulerpartlemgs2  34564  dstfrvel  34658  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemiex  34686  ballotlemfrcn0  34714  ballotlemirc  34716  ballotlem7  34720  reprsum  34797  reprsuc  34799  reprpmtf1o  34810  reprdifc  34811  fnrelpredd  35272  fineqvnttrclselem2  35303  connpconn  35463  iscvm  35487  cvmsi  35493  cvmsval  35494  cvmliftmolem2  35510  cvmliftiota  35529  snmlval  35559  satfv1lem  35590  fmlafvel  35613  fmla1  35615  fmlaomn0  35618  satfv0fvfmla0  35641  sategoelfvb  35647  elmpst  35764  lineelsb2  36376  linerflx1  36377  fwddifval  36390  fwddifnval  36391  rankeq1o  36399  finminlem  36546  fneint  36576  fnessref  36585  topmeet  36592  topjoin  36593  neifg  36599  weiunlem  36691  weiunfrlem  36692  weiunse  36696  regsfromregtco  36766  relowlssretop  37725  fin2solem  37973  fin2so  37974  poimirlem4  37991  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  opnmbllem0  38023  mblfinlem2  38025  itg2gt0cn  38042  indexa  38100  nninfnub  38118  istotbnd  38136  sstotbnd2  38141  isbnd  38147  isrngohom  38332  isrngoiso  38345  isidl  38381  ispridl  38401  ismaxidl  38407  prnc  38434  isfldidl  38435  islshp  39471  lssats  39504  islfl  39552  isat  39778  atlatmstc  39811  islln  39998  islpln  40022  islvol  40065  linepsubN  40244  elpmap  40250  pmapsub  40260  elpadd  40291  paddvaln0N  40293  islhp  40488  isldil  40602  isltrn  40611  isdilN  40646  istrnN  40649  diaval  41524  diaelval  41525  diaeldm  41528  diaelrnN  41537  cdlemm10N  41610  docaclN  41616  dibglbN  41658  dicval  41668  dicfnN  41675  dicvalrelN  41677  dihglblem2aN  41785  dihglblem2N  41786  dihglblem3N  41787  dih1dimatlem  41821  dihglb2  41834  dochvalr  41849  doch2val2  41856  dochocss  41858  islpolN  41975  mapd0  42157  aks4d1p4  42564  aks4d1p7  42568  isprimroot  42578  linvh  42581  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  sticksstones3  42633  aks6d1c6lem3  42657  grpods  42679  unitscyglem2  42681  unitscyglem4  42683  unitscyglem5  42684  supinf  42726  fsuppssindlem2  43042  infdesc  43093  isnacs  43153  elmzpcl  43175  mzpindd  43195  rencldnfilem  43265  irrapxlem6  43272  pellexlem3  43276  pellexlem5  43278  elpell1qr  43292  elpell14qr  43294  elpell1234qr  43296  pellfundre  43326  pellfundge  43327  pellfundlb  43329  pellfundglb  43330  rmspecnonsq  43352  jm2.22  43440  jm2.23  43441  rpnnen3lem  43476  fnwe2lem2  43496  elmnc  43581  dgraalem  43590  dgraaub  43593  mpaalem  43597  onsucelab  43708  limnsuc  43710  sqrtcvallem1  44075  rfovcnvf1od  44448  scottelrankd  44691  nzss  44761  iccshift  45963  iooshift  45967  limcperiod  46073  sumnnodd  46075  ioodvbdlimc1lem1  46374  dvnprodlem1  46389  dvnprodlem3  46391  itgperiod  46424  stoweidlem14  46457  stoweidlem15  46458  stoweidlem16  46459  stoweidlem31  46474  stoweidlem36  46479  stoweidlem46  46489  stoweidlem48  46491  fourierdlem2  46552  fourierdlem3  46553  fourierdlem20  46570  fourierdlem25  46575  fourierdlem37  46587  fourierdlem42  46592  fourierdlem48  46597  fourierdlem51  46600  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem79  46628  fourierdlem81  46630  elaa2lem  46676  etransclem24  46701  etransclem26  46703  etransclem28  46705  etransclem35  46712  etransclem48  46725  salgenval  46764  salgenn0  46774  salgencl  46775  sssalgen  46778  salgenss  46779  salgenuni  46780  issalgend  46781  salgencntex  46786  subsaliuncllem  46800  sge0fodjrnlem  46859  meadjiunlem  46908  caragenel  46938  ovnlecvr  47001  ovnpnfelsup  47002  ovncvrrp  47007  ovnsubaddlem1  47013  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem4  47041  ovnhoilem1  47044  ovnlecvr2  47053  ovncvr2  47054  issmflem  47170  smflimlem2  47215  smflimlem3  47216  smflimsuplem2  47264  elsetpreimafvrab  47869  iccpart  47891  sprel  47959  prelspr  47961  sprsymrelfolem2  47968  sprsymrelf  47970  prpair  47976  paireqne  47986  prprelb  47991  prprelprb  47992  dfodd2  48127  dfeven5  48157  dfodd7  48158  fpprel  48219  clnbgrel  48319  clnbupgrel  48325  sclnbgrel  48338  vopnbgrel  48345  dfclnbgr6  48347  dfnbgr6  48348  isubgredg  48357  uhgrimisgrgric  48422  grtriprop  48432  isgrtri  48434  stgredgel  48448  stgrusgra  48450  uspgrlimlem3  48481  uspgrlim  48483  grlimgredgex  48491  grlimgrtrilem2  48493  gpgiedgdmel  48540  gpgedgel  48541  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  gpgprismgr4cycllem10  48595  1hegrlfgr  48623  assintop  48700  isassintop  48701  assintopcllaw  48703  0even  48728  2even  48730  2zrngamgm  48736  dmatALTbasel  48893  lcoval  48903  elbigo  49042  elrrx2linest2  49236  itsclc0  49262  itsclc0b  49263  itscnhlinecirc02p  49276  unilbss  49308  secval  50237  cscval  50238  cotval  50239