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

Theorem elrab 3566
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
Hypothesis
Ref Expression
elrab.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elrab (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab
StepHypRef Expression
1 nfcv 2955 . 2 𝑥𝐴
2 nfcv 2955 . 2 𝑥𝐵
3 nfv 2005 . 2 𝑥𝜓
4 elrab.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
51, 2, 3, 4elrabf 3562 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  {crab 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112  df-v 3400
This theorem is referenced by:  elrab3  3567  elrabd  3568  elrab2  3569  ralrab  3571  rexrab  3573  rabsnt  4464  unimax  4674  ssintub  4694  intminss  4702  rabxfrd  5093  ssimaex  6487  weniso  6831  canth  6835  sorpsscmpl  7181  onnminsb  7237  dfom2  7300  ssnlim  7316  elsuppfn  7540  ressuppssdif  7553  oeeulem  7921  nnawordex  7957  elpmg  8111  fineqvlem  8416  mapfienlem2  8553  supub  8607  suplub  8608  ordtypelem6  8670  ordtypelem7  8671  hartogslem1  8689  hartogs  8691  wemapsolem  8697  card2on  8701  elharval  8710  wdom2d  8727  cantnfs  8813  oemapvali  8831  rankuni2b  8966  scottex  8998  tskwe  9062  cardid2  9065  iscard2  9088  harval2  9109  cardmin2  9110  acni3  9156  alephsuc2  9189  kmlem1  9260  cofsmo  9379  coftr  9383  fin23lem11  9427  enfin2i  9431  fin1a2lem9  9518  fin1a2lem11  9520  axcc4  9549  axdc3lem2  9561  zorn2lem7  9612  ondomon  9673  alephval2  9682  grutsk  9932  pinq  10037  negf1o  10748  fiminre  11260  infm3  11270  nnind  11326  peano2uz2  11734  peano5uzi  11735  dfuzi  11737  uzind  11738  uzind3  11740  eluz1  11911  uzind4  11967  nnwos  11977  eqreznegel  11996  zsupss  11999  zmin  12006  elixx1  12405  elioo2  12437  elfz1  12557  flval3  12843  serge0  13081  expge0  13122  expge1  13123  hashbclem  13456  pr2pwpr  13481  elss2prb  13489  hash2sspr  13490  wrdmap  13550  wwlktovfo  13929  shftf  14045  rlimrege0  14536  incexc2  14795  dvdsdivcl  15264  divalglem4  15342  divalgmod  15352  bitsval  15368  bezout  15482  dfgcd2  15485  lcmledvds  15534  lcmgcdlem  15541  lcmfledvds  15567  1nprm  15613  1idssfct  15614  isprm2  15616  phicl2  15693  hashdvds  15700  phisum  15715  odzval  15716  odzcllem  15717  odzdvds  15720  pcpremul  15768  prmreclem1  15840  prmreclem2  15841  prmreclem3  15842  prmreclem5  15844  ramub  15937  rami  15939  ramub1lem1  15950  ramub1lem2  15951  prmgaplem3  15977  prmgaplem4  15978  prmgaplem5  15979  prmgaplem6  15980  ismre  16458  mrcflem  16474  mrcval  16478  ismri  16499  isacs  16519  isacs1i  16525  catlid  16551  catrid  16552  ismon  16600  isnat  16814  eldmcoa  16922  coaval  16925  fncnvimaeqv  16967  lubeldm  17189  glbeldm  17202  gsumval2  17488  ismhm  17545  issubm  17555  issubmd  17557  mhmeql  17572  mrcmndind  17574  grplinv  17676  issubg  17799  cycsubg  17827  isnsg  17828  ghmeql  17888  isgim  17909  isga  17928  elcntz  17959  elcntzsn  17962  symgfix2  18040  pmtrval  18075  pmtrrn  18081  symgsssg  18091  symgfisg  18092  psgnunilem5  18118  odid  18161  odlem2  18162  gexid  18200  gexlem2  18201  gexdvds  18203  isslw  18227  pgpssslw  18233  pj1id  18316  efgsfo  18356  oddvdssubg  18462  dprdwd  18615  pgpfac1lem5  18683  ablfaclem2  18690  isirred  18904  isrim0  18930  issubrg  18987  isabv  19026  islss  19142  islmhm  19237  lmhmeql  19265  islmim  19272  islbs  19286  gsumbagdiaglem  19587  psrmulcllem  19599  psrlidm  19615  psrridm  19616  psrass1  19617  psrcom  19621  mplsubglem  19646  mpllsslem  19647  mplmonmul  19676  evlsval2  19731  coe1fsupp  19795  coe1ae0  19797  coe1mul2  19850  zrhcofipsgnOLD  20150  psgndiflemB  20157  elocv  20226  isobs  20278  dsmmelbas  20297  frlmelbas  20314  frlmssuvc2  20348  islinds  20362  dmatel  20514  dmatmulcl  20521  scmatel  20526  scmateALT  20533  symgmatr01lem  20675  pmatcoe1fsupp  20723  cpmatel  20733  chpscmat  20864  istopon  20934  fctop  21026  cctop  21028  ppttop  21029  pptbas  21030  epttop  21031  iscld  21049  clscld  21069  isnei  21125  neips  21135  neiptopnei  21154  iscn  21257  iscnp  21259  ordthauslem  21405  cmpsublem  21420  conncompconn  21453  2ndc1stc  21472  2ndcdisj  21477  locfincmp  21547  elkgen  21557  xkoopn  21610  xkoccn  21640  txdis1cn  21656  pthaus  21659  txkgen  21673  xkohaus  21674  xkococnlem  21680  xkococn  21681  xkoinjcn  21708  txconn  21710  elqtop  21718  nrmr0reg  21770  elmptrab  21848  fbssfi  21858  opnfbas  21863  elfg  21892  cfinfil  21914  csdfil  21915  supfil  21916  filssufilg  21932  uffix  21942  fixufil  21943  uffixfr  21944  uffixsn  21946  ufinffr  21950  ufilen  21951  elflim2  21985  supnfcls  22041  fclscf  22046  flimfnfcls  22049  alexsubALTlem2  22069  alexsubALTlem4  22071  alexsubALT  22072  ptcmplem2  22074  tmdgsum2  22117  symgtgp  22122  ghmcnp  22135  elutop  22254  isucn  22299  iscfilu  22309  ispsmet  22326  ismet  22345  isxmet  22346  elblps  22409  elbl  22410  restmetu  22592  icccmp  22845  elcncf  22909  ishtpy  22988  isphtpy  22997  om1elbas  23048  iscfil  23280  iscau  23291  iscmet  23299  lmle  23316  rrxfsupp  23403  minveclem3  23418  minveclem4  23421  ovolshftlem1  23496  ovolscalem1  23500  ovolicc2lem3  23506  iundisj  23535  dyadmax  23585  dyadmbllem  23586  opnmbllem  23588  vitalilem2  23596  vitalilem3  23597  elcpn  23917  ig1pval3  24154  coelem  24202  quotlem  24275  elqaalem1  24294  elqaalem3  24296  aannenlem1  24303  aannenlem2  24304  aalioulem2  24308  radcnv0  24390  dmarea  24904  jensen  24935  ftalem4  25022  ftalem5  25023  efnnfsumcl  25049  efchtdvds  25105  sqff1o  25128  fsumdvdsdiaglem  25129  dvdsppwf1o  25132  dvdsflf1o  25133  dvdsflsumcom  25134  musum  25137  muinv  25139  logfac2  25162  dchrelbas  25181  dchrfi  25200  lgsfle1  25251  lgsle1  25257  lgsdirprm  25276  lgsne0  25280  lgsquadlem1  25325  lgsquadlem2  25326  2lgslem1b  25337  dchrvmasumlem1  25404  logsqvma  25451  pntleml  25520  tgellng  25668  mircgr  25772  mirbtwn  25773  iseqlg  25967  ttgelitv  25983  upgrle  26205  upgrbi  26208  umgredg2  26215  umgrbi  26216  upgr1elem  26227  edgupgr  26249  edgumgr  26250  upgredg  26253  numedglnl  26260  edgusgr  26276  usgruspgrb  26297  usgredg2ALT  26306  ushgredgedg  26342  ushgredgedgloop  26344  ushgredgedgloopOLD  26345  usgrexmplef  26373  subumgredg2  26399  subupgr  26401  upgrreslem  26418  umgrreslem  26419  upgrres1  26427  nbgrel  26455  nbgrelOLD  26456  nbupgrel  26463  nbumgrvtx  26464  nbusgreledg  26471  nbgrnself  26477  uvtxaelOLD  26514  uvtxael1OLD  26525  uvtxusgrel  26532  1hevtxdg1  26636  umgr2v2e  26655  vtxdgoddnumeven  26683  rgrusgrprc  26719  rgrx0ndm  26723  lfgrwlkprop  26818  iswwlks  26963  iswwlksn  26965  wwlknonOLD  26989  wspthnonOLDOLD  26991  wwlksn0  26996  wlknwwlksnsurOLD  27023  wlkwwlksurOLD  27031  wwlksnextsur  27043  wlksnwwlknvbijOLD  27052  rusgrnumwwlkslem  27117  rusgrnumwwlks  27122  isclwwlk  27133  isclwwlknOLD  27180  clwwlknscsh  27219  eleclclwwlkn  27233  clwlknf1oclwwlkn  27254  isclwwlknonOLD  27264  s2elclwwlknon2  27278  clwwlkvbij  27288  clwwlkvbijOLDOLD  27289  clwwlkvbijOLD  27290  clwwlknunOLD  27292  eupth2lems  27417  konigsberglem4  27434  fusgreg2wsplem  27514  2clwwlkel  27532  numclwwlkovgelOLD  27535  extwwlkfabel  27538  clwwlknonclwlknonf1o  27548  dlwwlknondlwlknonf1o  27551  numclwwlk2lem1  27562  numclwlk2lem2f  27563  numclwlk2lem2f1o  27565  numclwwlk2lem1OLD  27569  numclwlk2lem2fOLD  27570  numclwlk2lem2f1oOLD  27572  grpoidinv2  27704  grpoinv  27714  isssp  27913  islno  27942  isblo  27971  ishmo  28000  ubthlem1  28060  ubthlem2  28061  htthlem  28108  ocel  28474  shsval2i  28580  ococin  28601  chsupsn  28606  eleigvec  29150  cnlnadjlem5  29264  shatomistici  29554  hatomistici  29555  nnindf  29898  ordtconnlem1  30301  indf1ofs  30419  sigagenval  30534  ldsysgenld  30554  ldgenpisyslem1  30557  ldgenpisyslem2  30558  ldgenpisys  30560  ddemeas  30630  ismbfm  30645  imambfm  30655  dya2iocuni  30676  oms0  30690  omssubadd  30693  elcarsg  30698  issibf  30726  sitgfval  30734  oddpwdc  30747  eulerpartlemgh  30771  eulerpartlemgs2  30773  dstfrvel  30866  ballotlemfc0  30885  ballotlemfcc  30886  ballotlemiex  30894  ballotlemfrcn0  30922  ballotlemirc  30924  ballotlem7  30928  reprsum  31022  reprsuc  31024  reprpmtf1o  31035  reprdifc  31036  connpconn  31545  iscvm  31569  cvmsi  31575  cvmsval  31576  cvmliftmolem2  31592  cvmliftiota  31611  snmlval  31641  elmpst  31761  sltval2  32135  sltres  32141  conway  32236  scutcut  32238  scutbday  32239  scutun12  32243  scutbdaybnd  32247  scutbdaylt  32248  lineelsb2  32581  linerflx1  32582  fwddifval  32595  fwddifnval  32596  rankeq1o  32604  finminlem  32638  fneint  32669  fnessref  32678  topmeet  32685  topjoin  32686  neifg  32692  relowlssretop  33529  fin2solem  33710  fin2so  33711  poimirlem4  33728  poimirlem25  33749  poimirlem26  33750  poimirlem27  33751  poimirlem31  33755  poimirlem32  33756  opnmbllem0  33760  mblfinlem2  33762  itg2gt0cn  33779  indexa  33842  nninfnub  33860  istotbnd  33881  sstotbnd2  33886  isbnd  33892  isrngohom  34077  isrngoiso  34090  isidl  34126  ispridl  34146  ismaxidl  34152  prnc  34179  isfldidl  34180  islshp  34761  lssats  34794  islfl  34842  isat  35068  atlatmstc  35101  islln  35288  islpln  35312  islvol  35355  linepsubN  35534  elpmap  35540  pmapsub  35550  elpadd  35581  paddvaln0N  35583  islhp  35778  isldil  35892  isltrn  35901  isdilN  35936  istrnN  35939  diaval  36814  diaelval  36815  diaeldm  36818  diaelrnN  36827  cdlemm10N  36900  docaclN  36906  dibglbN  36948  dicval  36958  dicfnN  36965  dicvalrelN  36967  dihglblem2aN  37075  dihglblem2N  37076  dihglblem3N  37077  dih1dimatlem  37111  dihglb2  37124  dochvalr  37139  doch2val2  37146  dochocss  37148  islpolN  37265  mapd0  37447  isnacs  37770  elmzpcl  37792  mzpindd  37812  rencldnfilem  37887  irrapxlem6  37894  pellexlem3  37898  pellexlem5  37900  elpell1qr  37914  elpell14qr  37916  elpell1234qr  37918  pellfundre  37948  pellfundge  37949  pellfundlb  37951  pellfundglb  37952  rmspecnonsq  37974  jm2.22  38064  jm2.23  38065  rpnnen3lem  38100  fnwe2lem2  38123  fnwe2lem3  38124  elmnc  38208  dgraalem  38217  dgraaub  38220  mpaalem  38224  rgspnmin  38243  issdrg  38269  rfovcnvf1od  38799  nzss  39017  iccshift  40226  iooshift  40230  limcperiod  40341  sumnnodd  40343  ioodvbdlimc1lem1  40627  dvnprodlem1  40642  dvnprodlem3  40644  itgperiod  40677  stoweidlem14  40711  stoweidlem15  40712  stoweidlem16  40713  stoweidlem31  40728  stoweidlem36  40733  stoweidlem46  40743  stoweidlem48  40745  fourierdlem2  40806  fourierdlem3  40807  fourierdlem20  40824  fourierdlem25  40829  fourierdlem37  40841  fourierdlem42  40846  fourierdlem48  40851  fourierdlem51  40854  fourierdlem63  40866  fourierdlem64  40867  fourierdlem65  40868  fourierdlem79  40882  fourierdlem81  40884  elaa2lem  40930  etransclem24  40955  etransclem26  40957  etransclem28  40959  etransclem35  40966  etransclem48  40979  salgenval  41021  salgenn0  41029  salgencl  41030  sssalgen  41033  salgenss  41034  salgenuni  41035  issalgend  41036  salgencntex  41041  subsaliuncllem  41055  sge0fodjrnlem  41113  meadjiunlem  41162  caragenel  41192  ovnlecvr  41255  ovnpnfelsup  41256  ovncvrrp  41261  ovnsubaddlem1  41267  hoidmv1lelem1  41288  hoidmv1lelem2  41289  hoidmv1lelem3  41290  hoidmvlelem1  41292  hoidmvlelem2  41293  hoidmvlelem4  41295  ovnhoilem1  41298  ovnlecvr2  41307  ovncvr2  41308  issmflem  41419  smflimlem2  41463  smflimlem3  41464  smflimsuplem2  41510  iccpart  41928  dfodd2  42125  dfeven5  42154  dfodd7  42155  1hegrlfgr  42282  sprel  42303  prelspr  42305  sprsymrelfolem2  42312  sprsymrelf  42314  ismgmhm  42352  issubmgm  42358  rabsubmgmd  42360  mgmhmeql  42372  assintop  42414  isassintop  42415  assintopcllaw  42417  isrnghm  42461  isrngisom  42465  0even  42500  2even  42502  2zrngamgm  42508  dmatALTbasel  42760  lcoval  42770  elbigo  42914  secval  43060  cscval  43061  cotval  43062
  Copyright terms: Public domain W3C validator