MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrab Structured version   Visualization version   GIF version

Theorem elrab 3678
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2383. (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
StepHypRef Expression
1 elex 3511 . 2 (𝐴 ∈ {𝑥𝐵𝜑} → 𝐴 ∈ V)
2 elex 3511 . . 3 (𝐴𝐵𝐴 ∈ V)
32adantr 483 . 2 ((𝐴𝐵𝜓) → 𝐴 ∈ V)
4 eleq1 2898 . . . 4 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
5 elrab.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
64, 5anbi12d 632 . . 3 (𝑥 = 𝐴 → ((𝑥𝐵𝜑) ↔ (𝐴𝐵𝜓)))
7 df-rab 3145 . . 3 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
86, 7elab2g 3666 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓)))
91, 3, 8pm5.21nii 382 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1530  wcel 2107  {crab 3140  Vcvv 3493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495
This theorem is referenced by:  elrab3  3679  elrabd  3680  elrab2  3681  ralrab  3683  rexrab  3685  rabsnt  4659  unimax  4865  ssintub  4885  intminss  4893  rabxfrd  5308  ssimaex  6741  weniso  7099  canth  7103  sorpsscmpl  7452  onnminsb  7511  dfom2  7574  ssnlim  7591  elsuppfn  7830  ressuppssdif  7843  oeeulem  8219  elpmg  8414  fineqvlem  8724  mapfienlem2  8861  supub  8915  suplub  8916  ordtypelem6  8979  ordtypelem7  8980  hartogslem1  8998  hartogs  9000  wemapsolem  9006  card2on  9010  elharval  9019  wdom2d  9036  cantnfs  9121  scottex  9306  tskwe  9371  cardid2  9374  iscard2  9397  cardmin2  9419  acni3  9465  alephsuc2  9498  kmlem1  9568  cofsmo  9683  coftr  9687  fin23lem11  9731  enfin2i  9735  fin1a2lem9  9822  fin1a2lem11  9824  axcc4  9853  axdc3lem2  9865  zorn2lem7  9916  ondomon  9977  alephval2  9986  grutsk  10236  negf1o  11062  fiminreOLD  11582  infm3  11592  nnind  11648  peano2uz2  12062  peano5uzi  12063  dfuzi  12065  uzind  12066  uzind3  12068  eluz1  12239  uzind4  12298  nnwos  12307  eqreznegel  12326  zmin  12336  elixx1  12739  elioo2  12771  elfz1  12889  flval3  13177  serge0  13416  expge0  13457  expge1  13458  hashbclem  13802  pr2pwpr  13829  elss2prb  13837  hash2sspr  13838  wrdmap  13889  wwlktovfo  14314  shftf  14430  rlimrege0  14928  incexc2  15185  dvdsdivcl  15658  divalglem4  15739  divalgmod  15749  bitsval  15765  bezout  15883  dfgcd2  15886  lcmledvds  15935  lcmgcdlem  15942  lcmfledvds  15968  1nprm  16015  1idssfct  16016  isprm2  16018  hashdvds  16104  phisum  16119  odzval  16120  odzcllem  16121  odzdvds  16124  prmreclem2  16245  prmreclem5  16248  rami  16343  ramub1lem1  16354  ramub1lem2  16355  prmgaplem3  16381  prmgaplem4  16382  prmgaplem5  16383  prmgaplem6  16384  ismre  16853  ismri  16894  isacs  16914  isacs1i  16920  catlid  16946  catrid  16947  ismon  16995  isnat  17209  eldmcoa  17317  fncnvimaeqv  17362  lubeldm  17583  glbeldm  17596  gsumval2  17888  ismhm  17950  issubm  17960  issubmd  17963  mndind  17984  grplinv  18144  issubg  18271  isnsg  18299  cycsubg  18343  isgim  18394  isga  18413  elcntz  18444  elcntzsn  18447  symgfix2  18536  symgsssg  18587  symgfisg  18588  psgnunilem5  18614  odid  18658  odlem2  18659  gexid  18698  gexlem2  18699  gexdvds  18701  isslw  18725  pgpssslw  18731  pj1id  18817  oddvdssubg  18967  pgpfac1lem5  19193  ablfaclem2  19200  isirred  19441  isrim0  19467  issubrg  19527  issdrg  19566  isabv  19582  islss  19698  islmhm  19791  islmim  19826  islbs  19840  gsumbagdiaglem  20147  psrmulcllem  20159  psrlidm  20175  psrridm  20176  psrass1  20177  psrcom  20181  mplsubglem  20206  mpllsslem  20207  evlsval2  20292  ismhp  20326  coe1ae0  20376  coe1mul2  20429  psgndiflemB  20736  elocv  20804  isobs  20856  dsmmelbas  20875  frlmelbas  20892  islinds  20945  dmatel  21094  scmatel  21106  scmateALT  21113  symgmatr01lem  21254  pmatcoe1fsupp  21301  cpmatel  21311  chpscmat  21442  istopon  21512  fctop  21604  cctop  21606  ppttop  21607  pptbas  21608  epttop  21609  iscld  21627  clscld  21647  isnei  21703  neips  21713  neiptopnei  21732  iscn  21835  iscnp  21837  cmpsublem  21999  conncompconn  22032  2ndc1stc  22051  2ndcdisj  22056  elkgen  22136  xkoccn  22219  txdis1cn  22235  txkgen  22252  xkococnlem  22259  xkococn  22260  xkoinjcn  22287  txconn  22289  elqtop  22297  elmptrab  22427  fbssfi  22437  opnfbas  22442  elfg  22471  cfinfil  22493  csdfil  22494  supfil  22495  filssufilg  22511  uffix  22521  fixufil  22522  uffixfr  22523  elflim2  22564  fclscf  22625  flimfnfcls  22628  alexsubALTlem2  22648  alexsubALTlem4  22650  alexsubALT  22651  ptcmplem2  22653  elutop  22834  isucn  22879  iscfilu  22889  ispsmet  22906  ismet  22925  isxmet  22926  elblps  22989  elbl  22990  restmetu  23172  icccmp  23425  elcncf  23489  ishtpy  23568  isphtpy  23577  om1elbas  23628  iscfil  23860  iscau  23871  iscmet  23879  lmle  23896  rrxfsupp  23997  minveclem3  24024  minveclem4  24027  ovolshftlem1  24102  ovolscalem1  24106  ovolicc2lem3  24112  dyadmax  24191  dyadmbllem  24192  opnmbllem  24194  vitalilem2  24202  vitalilem3  24203  elcpn  24523  ig1pval3  24760  coelem  24808  quotlem  24881  elqaalem1  24900  elqaalem3  24902  aannenlem1  24909  aannenlem2  24910  dmarea  25527  jensen  25558  ftalem4  25645  efnnfsumcl  25672  efchtdvds  25728  sqff1o  25751  fsumdvdsdiaglem  25752  dvdsppwf1o  25755  dvdsflf1o  25756  dvdsflsumcom  25757  musum  25760  muinv  25762  logfac2  25785  dchrelbas  25804  lgsfle1  25874  lgsle1  25880  lgsdirprm  25899  lgsne0  25903  lgsquadlem1  25948  lgsquadlem2  25949  dchrvmasumlem1  26063  logsqvma  26110  pntleml  26179  tgellng  26331  mircgr  26435  mirbtwn  26436  iseqlg  26645  ttgelitv  26661  upgrle  26867  upgrbi  26870  umgredg2  26877  umgrbi  26878  edgupgr  26911  edgumgr  26912  upgredg  26914  numedglnl  26921  edgusgr  26937  usgruspgrb  26958  usgredg2ALT  26967  ushgredgedg  27003  ushgredgedgloop  27005  usgrexmplef  27033  upgrreslem  27078  umgrreslem  27079  upgrres1  27087  nbgrel  27114  nbupgrel  27119  nbumgrvtx  27120  nbusgreledg  27127  nbgrnself  27133  uvtxusgrel  27177  vtxdgoddnumeven  27327  rgrusgrprc  27363  lfgrwlkprop  27461  iswwlks  27606  iswwlksn  27608  wwlksnextsurj  27670  rusgrnumwwlkslem  27740  rusgrnumwwlks  27745  isclwwlk  27754  clwwlknscsh  27833  eleclclwwlkn  27847  clwlknf1oclwwlkn  27855  clwwlkvbij  27884  eupth2lems  28009  konigsberglem4  28026  fusgreg2wsplem  28104  2clwwlkel  28120  extwwlkfabel  28124  clwwlknonclwlknonf1o  28133  dlwwlknondlwlknonf1o  28136  numclwwlk2lem1  28147  numclwlk2lem2f  28148  numclwlk2lem2f1o  28150  grpoidinv2  28284  grpoinv  28294  isssp  28493  islno  28522  isblo  28551  ishmo  28580  ubthlem1  28639  ubthlem2  28640  htthlem  28686  ocel  29050  shsval2i  29156  ococin  29177  chsupsn  29182  eleigvec  29726  cnlnadjlem5  29840  shatomistici  30130  hatomistici  30131  dmrab  30252  nnindf  30527  tocycf  30752  tocyc01  30753  trsp2cyc  30758  cycpmco2f1  30759  cycpmco2rn  30760  cycpmco2lem2  30762  cycpmco2lem3  30763  cycpmco2lem5  30765  cycpmco2lem6  30766  cycpmco2lem7  30767  cycpmconjv  30777  tocyccntz  30779  cyc3evpm  30785  cycpmgcl  30788  cycpmconjslem2  30790  cyc3conja  30792  isprmidl  30948  ismxidl  30963  fedgmullem2  31014  ordtconnlem1  31155  indf1ofs  31273  sigagenval  31387  ldsysgenld  31407  ldgenpisyslem1  31410  ldgenpisyslem2  31411  ldgenpisys  31413  ddemeas  31483  ismbfm  31498  imambfm  31508  dya2iocuni  31529  oms0  31543  omssubadd  31546  elcarsg  31551  issibf  31579  sitgfval  31587  oddpwdc  31600  eulerpartlemgh  31624  eulerpartlemgs2  31626  dstfrvel  31719  ballotlemfc0  31738  ballotlemfcc  31739  ballotlemiex  31747  ballotlemfrcn0  31775  ballotlemirc  31777  ballotlem7  31781  reprsum  31872  reprsuc  31874  reprpmtf1o  31885  reprdifc  31886  connpconn  32470  iscvm  32494  cvmsi  32500  cvmsval  32501  cvmliftmolem2  32517  cvmliftiota  32536  snmlval  32566  satfv1lem  32597  fmlafvel  32620  fmla1  32622  fmlaomn0  32625  satfv0fvfmla0  32648  sategoelfvb  32654  elmpst  32771  sltval2  33151  sltres  33157  conway  33252  scutcut  33254  scutbday  33255  scutun12  33259  scutbdaybnd  33263  scutbdaylt  33264  lineelsb2  33597  linerflx1  33598  fwddifval  33611  fwddifnval  33612  rankeq1o  33620  finminlem  33654  fneint  33684  fnessref  33693  topmeet  33700  topjoin  33701  neifg  33707  relowlssretop  34631  fin2solem  34865  fin2so  34866  poimirlem4  34883  poimirlem25  34904  poimirlem26  34905  poimirlem27  34906  poimirlem31  34910  poimirlem32  34911  opnmbllem0  34915  mblfinlem2  34917  itg2gt0cn  34934  indexa  34995  nninfnub  35013  istotbnd  35034  sstotbnd2  35039  isbnd  35045  isrngohom  35230  isrngoiso  35243  isidl  35279  ispridl  35299  ismaxidl  35305  prnc  35332  isfldidl  35333  islshp  36102  lssats  36135  islfl  36183  isat  36409  atlatmstc  36442  islln  36629  islpln  36653  islvol  36696  linepsubN  36875  elpmap  36881  pmapsub  36891  elpadd  36922  paddvaln0N  36924  islhp  37119  isldil  37233  isltrn  37242  isdilN  37277  istrnN  37280  diaval  38155  diaelval  38156  diaeldm  38159  diaelrnN  38168  cdlemm10N  38241  docaclN  38247  dibglbN  38289  dicval  38299  dicfnN  38306  dicvalrelN  38308  dihglblem2aN  38416  dihglblem2N  38417  dihglblem3N  38418  dih1dimatlem  38452  dihglb2  38465  dochvalr  38480  doch2val2  38487  dochocss  38489  islpolN  38606  mapd0  38788  isnacs  39286  elmzpcl  39308  mzpindd  39328  rencldnfilem  39402  irrapxlem6  39409  pellexlem3  39413  pellexlem5  39415  elpell1qr  39429  elpell14qr  39431  elpell1234qr  39433  pellfundre  39463  pellfundge  39464  pellfundlb  39466  pellfundglb  39467  rmspecnonsq  39489  jm2.22  39577  jm2.23  39578  rpnnen3lem  39613  fnwe2lem2  39636  elmnc  39721  dgraalem  39730  dgraaub  39733  mpaalem  39737  rgspnmin  39756  rfovcnvf1od  40335  scottelrankd  40568  nzss  40634  iccshift  41778  iooshift  41782  limcperiod  41893  sumnnodd  41895  ioodvbdlimc1lem1  42200  dvnprodlem1  42215  dvnprodlem3  42217  itgperiod  42250  stoweidlem14  42284  stoweidlem15  42285  stoweidlem16  42286  stoweidlem31  42301  stoweidlem36  42306  stoweidlem46  42316  stoweidlem48  42318  fourierdlem2  42379  fourierdlem3  42380  fourierdlem20  42397  fourierdlem25  42402  fourierdlem37  42414  fourierdlem42  42419  fourierdlem48  42424  fourierdlem51  42427  fourierdlem63  42439  fourierdlem64  42440  fourierdlem65  42441  fourierdlem79  42455  fourierdlem81  42457  elaa2lem  42503  etransclem24  42528  etransclem26  42530  etransclem28  42532  etransclem35  42539  etransclem48  42552  salgenval  42591  salgenn0  42599  salgencl  42600  sssalgen  42603  salgenss  42604  salgenuni  42605  issalgend  42606  salgencntex  42611  subsaliuncllem  42625  sge0fodjrnlem  42683  meadjiunlem  42732  caragenel  42762  ovnlecvr  42825  ovnpnfelsup  42826  ovncvrrp  42831  ovnsubaddlem1  42837  hoidmv1lelem1  42858  hoidmv1lelem2  42859  hoidmv1lelem3  42860  hoidmvlelem1  42862  hoidmvlelem2  42863  hoidmvlelem4  42865  ovnhoilem1  42868  ovnlecvr2  42877  ovncvr2  42878  issmflem  42989  smflimlem2  43033  smflimlem3  43034  smflimsuplem2  43080  elsetpreimafvrab  43539  iccpart  43561  sprel  43631  prelspr  43633  sprsymrelfolem2  43640  sprsymrelf  43642  prpair  43648  paireqne  43658  prprelb  43663  prprelprb  43664  dfodd2  43786  dfeven5  43816  dfodd7  43817  fpprel  43878  1hegrlfgr  43992  ismgmhm  44035  issubmgm  44041  rabsubmgmd  44043  mgmhmeql  44055  assintop  44101  isassintop  44102  assintopcllaw  44104  isrnghm  44148  isrngisom  44152  0even  44187  2even  44189  2zrngamgm  44195  dmatALTbasel  44442  lcoval  44452  elbigo  44596  elrrx2linest2  44717  itsclc0  44743  itsclc0b  44744  itscnhlinecirc02p  44757  secval  44831  cscval  44832  cotval  44833
  Copyright terms: Public domain W3C validator