Theorem elrab 3648

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {crab 3416  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456

This theorem is used by:  elrab3  3649  elrabd  3650  elrabrd  3651  elrab2  3652  ralrab  3655  rexrab  3657  reurab  3662  rabsnt  4694  unimax  4910  ssintub  4931  intminss  4939  rabxfrd  5386  ssimaex  7001  weniso  7395  canth  7405  riotarab  7450  sorpsscmpl  7782  onnminsb  7847  dfom2  7913  ssnlim  7931  fnwe2lem3  8184  elsuppfng  8224  elsuppfn  8225  ressuppssdif  8240  oeeulem  8648  cofonr  8721  elpmg  8901  fineqvlem  9295  mapfienlem2  9435  supub  9488  suplub  9489  ordtypelem6  9554  ordtypelem7  9555  hartogslem1  9573  hartogs  9575  wemapsolem  9581  card2on  9585  elharval  9592  wdom2d  9611  cantnfs  9704  scottex  9970  scottexOLD  9971  scottelrankd  9985  tskwe  10068  cardid2  10071  iscard2  10094  cardmin2  10119  acni3  10165  alephsuc2  10198  kmlem1  10268  cofsmo  10386  coftr  10390  fin23lem11  10434  enfin2i  10438  fin1a2lem9  10525  fin1a2lem11  10527  axcc4  10556  axdc3lem2  10568  zorn2lem7  10619  ondomon  10686  alephval2  10696  grutsk  10946  negf1o  11785  infm3  12316  nnind  12393  peano2uz2  12827  peano5uzi  12828  dfuzi  12830  uzind  12831  uzind3  12833  eluz1  13009  uzind4  13073  nnwos  13082  eqreznegel  13101  zmin  13111  elixx1  13525  elioo2  13557  elfz1  13684  flval3  13995  serge0  14239  expge0  14281  expge1  14282  hashbclem  14638  pr2pwpr  14665  elss2prb  14674  hash2sspr  14675  wrdmap  14732  wwlktovfo  15154  shftf  15275  rlimrege0  15790  incexc2  16051  dvdsdivcl  16530  divalglem4  16610  divalgmod  16620  bitsval  16638  bezout  16760  dfgcd2  16763  lcmledvds  16818  lcmgcdlem  16825  lcmfledvds  16851  1nprm  16898  1idssfct  16899  isprm2  16901  hashdvds  16996  phisum  17012  odzval  17013  odzcllem  17014  odzdvds  17017  prmreclem2  17139  prmreclem5  17142  rami  17237  ramub1lem1  17248  ramub1lem2  17249  prmgaplem3  17275  prmgaplem4  17276  prmgaplem5  17277  prmgaplem6  17278  ismre  17810  ismri  17855  isacs  17875  isacs1i  17881  catlid  17907  catrid  17908  ismon  17958  isnat  18175  eldmcoa  18290  fncnvimaeqv  18344  lubeldm  18575  glbeldm  18588  gsumval2  18925  ismgmhm  18935  issubmgm  18941  rabsubmgmd  18943  mgmhmeql  18955  ismhm  19030  issubm  19048  issubmd  19051  mndind  19074  grplinv  19250  issubg  19386  isnsg  19415  cycsubg  19473  isgim  19526  isga  19556  elcntz  19587  elcntzsn  19590  symgfix2  19681  symgsssg  19732  symgfisg  19733  psgnunilem5  19759  odid  19803  odlem2  19804  gexid  19846  gexlem2  19847  gexdvds  19849  isslw  19873  pgpssslw  19879  pj1id  19964  oddvdssubg  20120  pgpfac1lem5  20346  ablfaclem2  20353  isirred  20700  isrnghm  20722  isrngim  20726  isrhm0  20757  isrim0  20764  rimval  20781  issubrng  20850  issubrg  20874  rgspnmin  20918  issdrg  21096  isabv  21119  islss  21260  islmhm  21353  islmim  21388  islbs  21402  isprmidl  21670  psgndiflemB  21961  elocv  22029  isobs  22081  dsmmelbas  22100  frlmelbas  22117  islinds  22170  gsumbagdiaglem  22294  rhmpsrlem2  22304  psrlidm  22324  psrridm  22325  psrass1  22326  psrcom  22330  mplsubglem  22361  mpllsslem  22362  evlsval2  22451  ismhp  22516  ismhp3  22518  mhpmulcl  22525  psdmul  22542  coe1ae0  22589  coe1mul2  22643  dmatel  22863  scmatel  22875  scmateALT  22882  symgmatr01lem  23023  pmatcoe1fsupp  23074  cpmatel  23084  chpscmat  23215  istopon  23285  fctop  23377  cctop  23379  ppttop  23380  pptbas  23381  epttop  23382  iscld  23400  clscld  23420  isnei  23476  neips  23486  neiptopnei  23505  iscn  23608  iscnp  23610  cmpsublem  23772  conncompconn  23805  2ndc1stc  23824  2ndcdisj  23830  elkgen  23910  xkoccn  23993  txdis1cn  24009  txkgen  24026  xkococnlem  24033  xkococn  24034  xkoinjcn  24061  txconn  24063  elqtop  24071  elmptrab  24201  fbssfi  24211  opnfbas  24216  elfg  24245  cfinfil  24267  csdfil  24268  supfil  24269  filssufilg  24285  uffix  24295  fixufil  24296  uffixfr  24297  elflim2  24338  fclscf  24399  flimfnfcls  24402  alexsubALTlem2  24422  alexsubALTlem4  24424  alexsubALT  24425  ptcmplem2  24427  elutop  24607  isucn  24651  iscfilu  24661  ispsmet  24678  ismet  24697  isxmet  24698  elblps  24761  elbl  24762  restmetu  24944  icccmp  25200  elcncf  25265  ishtpy  25348  isphtpy  25357  om1elbas  25408  iscfil  25641  iscau  25652  iscmet  25660  lmle  25677  rrxfsupp  25778  minveclem3  25805  minveclem4  25808  ovolshftlem1  25885  ovolscalem1  25889  ovolicc2lem3  25895  dyadmax  25974  dyadmbllem  25975  opnmbllem  25977  vitalilem2  25985  vitalilem3  25986  elcpn  26309  ig1pval3  26551  coelem  26600  quotlem  26676  elqaalem1  26699  elqaalem3  26701  aannenlem1  26712  aannenlem2  26713  dmarea  27342  jensen  27373  ftalem4  27460  efnnfsumcl  27487  efchtdvds  27543  sqff1o  27566  fsumdvdsdiaglem  27567  dvdsppwf1o  27570  dvdsflf1o  27571  dvdsflsumcom  27572  musum  27575  muinv  27577  logfac2  27601  dchrelbas  27620  lgsfle1  27690  lgsle1  27696  lgsdirprm  27715  lgsne0  27719  lgsquadlem1  27764  lgsquadlem2  27765  dchrvmasumlem1  27879  logsqvma  27926  pntleml  27995  infdesc  28024  ltsval2  28070  ltsres  28076  conway  28222  cutcuts  28224  cutbday  28227  cutsun12  28233  cutbdaybnd2  28239  cutbdaylt  28241  bday1  28257  cutlt  28375  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  oncutlt  28707  noseqinds  28736  peano5uzs  28847  uzsind  28848  tgellng  29073  mircgr  29186  mirbtwn  29187  elplng  29315  iseqlg  29469  ttgelitv  29517  upgrle  29725  upgrbi  29728  umgredg2  29735  umgrbi  29736  edgupgr  29769  edgumgr  29770  upgredg  29772  numedglnl  29779  edgusgr  29798  usgruspgrb  29821  usgredg2ALT  29831  ushgredgedg  29867  ushgredgedgloop  29869  usgrexmplef  29897  upgrreslem  29942  umgrreslem  29943  upgrres1  29951  nbgrel  29978  nbupgrel  29983  nbumgrvtx  29984  nbusgreledg  29991  nbgrnself  29997  uvtxusgrel  30041  vtxdgoddnumeven  30191  rgrusgrprc  30227  lfgrwlkprop  30327  iswwlks  30482  iswwlksn  30484  wwlksnextsurj  30546  rusgrnumwwlkslem  30618  rusgrnumwwlks  30623  isclwwlk  30632  clwwlknscsh  30710  eleclclwwlkn  30724  clwlknf1oclwwlkn  30732  clwwlkvbij  30761  eupth2lems  30896  konigsberglem4  30913  fusgreg2wsplem  30991  2clwwlkel  31007  extwwlkfabel  31011  clwwlknonclwlknonf1o  31020  dlwwlknondlwlknonf1o  31023  numclwwlk2lem1  31034  numclwlk2lem2f  31035  numclwlk2lem2f1o  31037  grpoidinv2  31174  grpoinv  31184  isssp  31383  islno  31412  isblo  31441  ishmo  31470  ubthlem1  31529  ubthlem2  31530  htthlem  31576  ocel  31940  shsval2i  32046  ococin  32067  chsupsn  32072  eleigvec  32616  cnlnadjlem5  32730  shatomistici  33020  hatomistici  33021  dmrab  33192  nnindf  33507  indf1ofs  33529  ismnt  33643  pwrssmgc  33660  tocycf  33777  tocyc01  33778  trsp2cyc  33783  cycpmco2f1  33784  cycpmco2rn  33785  cycpmco2lem2  33787  cycpmco2lem3  33788  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmconjv  33802  tocyccntz  33804  cyc3evpm  33810  cycpmgcl  33813  cyc3conja  33817  isfxp  33828  fxpgaeq  33829  elrgspnsubrun  33909  rlocisunit  33936  fldgensdrg  33980  nsgmgclem  34066  nsgmgc  34067  nsgqusf1olem2  34069  ismxidl  34091  ssmxidl  34103  isrprm  34153  1arithufdlem3  34182  1arithufdlem4  34183  1arithufd  34184  mplvrpmga  34288  mplvrpmmhm  34289  fedgmullem2  34373  ply1annnr  34446  minplyann  34452  minplyirred  34454  constrsuc  34481  zarclsiin  34614  zart0  34622  rhmpreimacnlem  34627  ordtconnlem1  34667  sigagenval  34884  ldsysgenld  34904  ldgenpisyslem1  34907  ldgenpisyslem2  34908  ldgenpisys  34910  ddemeas  34980  ismbfm  34995  imambfm  35005  dya2iocuni  35026  oms0  35040  omssubadd  35043  elcarsg  35048  issibf  35076  sitgfval  35084  oddpwdc  35097  eulerpartlemgh  35121  eulerpartlemgs2  35123  dstfrvel  35217  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemiex  35245  ballotlemfrcn0  35273  ballotlemirc  35275  ballotlem7  35279  reprsum  35353  reprsuc  35355  reprpmtf1o  35366  reprdifc  35367  fnrelpredd  35845  fineqvnttrclselem2  35931  connpconn  36208  iscvm  36232  cvmsi  36238  cvmsval  36239  cvmliftmolem2  36255  cvmliftiota  36274  snmlval  36304  satfv1lem  36335  fmlafvel  36358  fmla1  36360  fmlaomn0  36363  satfv0fvfmla0  36386  sategoelfvb  36392  elmpst  36509  lineelsb2  37128  linerflx1  37129  fwddifval  37142  fwddifnval  37143  rankeq1o  37147  finminlem  37321  fneint  37351  fnessref  37360  topmeet  37367  topjoin  37368  neifg  37374  weiunlem  37466  weiunfrlem  37467  weiunse  37471  regsfromregtco  37541  relowlssretop  38554  fin2solem  38797  fin2so  38798  poimirlem4  38810  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  opnmbllem0  38842  mblfinlem2  38844  itg2gt0cn  38861  indexa  38935  nninfnub  38951  istotbnd  38969  sstotbnd2  38974  isbnd  38980  isrngohom  39165  isrngoiso  39178  isidl  39214  ispridl  39234  ismaxidl  39240  prnc  39267  isfldidl  39268  islshp  40302  lssats  40335  islfl  40383  isat  40609  atlatmstc  40642  islln  40829  islpln  40853  islvol  40896  linepsubN  41075  elpmap  41081  pmapsub  41091  elpadd  41122  paddvaln0N  41124  islhp  41319  isldil  41433  isltrn  41442  isdilN  41477  istrnN  41480  diaval  42355  diaelval  42356  diaeldm  42359  diaelrnN  42368  cdlemm10N  42441  docaclN  42447  dibglbN  42489  dicval  42499  dicfnN  42506  dicvalrelN  42508  dihglblem2aN  42616  dihglblem2N  42617  dihglblem3N  42618  dih1dimatlem  42652  dihglb2  42665  dochvalr  42680  doch2val2  42687  dochocss  42689  islpolN  42806  mapd0  42988  aks4d1p4  43395  aks4d1p7  43399  isprimroot  43409  linvh  43412  primrootsunit1  43413  primrootscoprmpow  43415  primrootscoprbij  43418  sticksstones3  43464  aks6d1c6lem3  43488  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  unitscyglem5  43515  supinf  43560  fsuppssindlem2  43886  isnacs  43981  elmzpcl  44003  mzpindd  44023  rencldnfilem  44093  irrapxlem6  44100  pellexlem3  44104  pellexlem5  44106  elpell1qr  44120  elpell14qr  44122  elpell1234qr  44124  pellfundre  44154  pellfundge  44155  pellfundlb  44157  pellfundglb  44158  rmspecnonsq  44180  jm2.22  44268  jm2.23  44269  rpnnen3lem  44304  elmnc  44403  dgraalem  44412  dgraaub  44415  mpaalem  44419  onsucelab  44526  limnsuc  44528  sqrtcvallem1  44892  rfovcnvf1od  45265  nzss  45562  iccshift  46803  iooshift  46807  limcperiod  46913  sumnnodd  46915  ioodvbdlimc1lem1  47214  dvnprodlem1  47229  dvnprodlem3  47231  itgperiod  47264  stoweidlem14  47297  stoweidlem15  47298  stoweidlem16  47299  stoweidlem31  47314  stoweidlem36  47319  stoweidlem46  47329  stoweidlem48  47331  fourierdlem2  47392  fourierdlem3  47393  fourierdlem20  47410  fourierdlem25  47415  fourierdlem37  47427  fourierdlem42  47432  fourierdlem48  47437  fourierdlem51  47440  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem79  47468  fourierdlem81  47470  elaa2lem  47516  etransclem24  47541  etransclem26  47543  etransclem28  47545  etransclem35  47552  etransclem48  47565  salgenval  47604  salgenn0  47614  salgencl  47615  sssalgen  47618  salgenss  47619  salgenuni  47620  issalgend  47621  salgencntex  47626  subsaliuncllem  47640  sge0fodjrnlem  47699  meadjiunlem  47748  caragenel  47778  ovnlecvr  47841  ovnpnfelsup  47842  ovncvrrp  47847  ovnsubaddlem1  47853  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem4  47881  ovnhoilem1  47884  ovnlecvr2  47893  ovncvr2  47894  issmflem  48010  smflimlem2  48055  smflimlem3  48056  smflimsuplem2  48104  elsetpreimafvrab  48749  iccpart  48771  sprel  48839  prelspr  48841  sprsymrelfolem2  48848  sprsymrelf  48850  prpair  48856  paireqne  48866  prprelb  48871  prprelprb  48872  dfodd2  49007  dfeven5  49037  dfodd7  49038  fpprel  49099  clnbgrel  49199  clnbupgrel  49205  sclnbgrel  49218  vopnbgrel  49225  dfclnbgr6  49227  dfnbgr6  49228  isubgredg  49237  uhgrimisgrgric  49302  grtriprop  49312  isgrtri  49314  stgredgel  49328  stgrusgra  49330  uspgrlimlem3  49361  uspgrlim  49363  grlimgredgex  49371  grlimgrtrilem2  49373  gpgiedgdmel  49420  gpgedgel  49421  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  gpgprismgr4cycllem10  49475  1hegrlfgr  49503  assintop  49579  isassintop  49580  assintopcllaw  49582  0even  49607  2even  49609  2zrngamgm  49615  dmatALTbasel  49845  lcoval  49855  elbigo  49994  elrrx2linest2  50188  itsclc0  50214  itsclc0b  50215  itscnhlinecirc02p  50228  unilbss  50260  secval  51268  cscval  51269  cotval  51270  dvsec  51284  dvcsc  51285  dvcot  51286