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

Theorem elrab 3357
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 2762 . 2 𝑥𝐴
2 nfcv 2762 . 2 𝑥𝐵
3 nfv 1841 . 2 𝑥𝜓
4 elrab.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
51, 2, 3, 4elrabf 3354 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  {crab 2913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197
This theorem is referenced by:  elrab3  3358  elrabd  3359  elrab2  3360  ralrab  3362  rexrab  3364  rabsnt  4257  unimax  4464  ssintub  4486  intminss  4494  rabxfrd  4880  ssimaex  6250  weniso  6589  canth  6593  sorpsscmpl  6933  onnminsb  6989  dfom2  7052  ssnlim  7068  elsuppfn  7288  ressuppssdif  7301  oeeulem  7666  nnawordex  7702  elpmg  7858  fineqvlem  8159  mapfienlem2  8296  supub  8350  suplub  8351  ordtypelem6  8413  ordtypelem7  8414  hartogslem1  8432  hartogs  8434  wemapsolem  8440  card2on  8444  elharval  8453  wdom2d  8470  cantnfs  8548  oemapvali  8566  rankuni2b  8701  scottex  8733  tskwe  8761  cardid2  8764  iscard2  8787  harval2  8808  cardmin2  8809  acni3  8855  alephsuc2  8888  kmlem1  8957  cofsmo  9076  coftr  9080  fin23lem11  9124  enfin2i  9128  fin1a2lem9  9215  fin1a2lem11  9217  axcc4  9246  axdc3lem2  9258  zorn2lem7  9309  ondomon  9370  alephval2  9379  grutsk  9629  pinq  9734  negf1o  10445  fiminre  10957  infm3  10967  nnind  11023  peano2uz2  11450  peano5uzi  11451  dfuzi  11453  uzind  11454  uzind3  11456  eluz1  11676  uzind4  11731  nnwos  11740  eqreznegel  11759  zsupss  11762  zmin  11769  elixx1  12169  elioo2  12201  elfz1  12316  flval3  12599  serge0  12838  expge0  12879  expge1  12880  hashbclem  13219  pr2pwpr  13244  elss2prb  13252  hash2sspr  13253  wrdmap  13319  wwlktovfo  13682  shftf  13800  rlimrege0  14291  incexc2  14551  dvdsdivcl  15019  divalglem4  15100  divalgmod  15110  divalgmodOLD  15111  bitsval  15127  bezout  15241  dfgcd2  15244  lcmledvds  15293  lcmgcdlem  15300  lcmfledvds  15326  1nprm  15373  1idssfct  15374  isprm2  15376  phicl2  15454  hashdvds  15461  phisum  15476  odzval  15477  odzcllem  15478  odzdvds  15481  pcpremul  15529  prmreclem1  15601  prmreclem2  15602  prmreclem3  15603  prmreclem5  15605  ramub  15698  rami  15700  ramub1lem1  15711  ramub1lem2  15712  prmgaplem3  15738  prmgaplem4  15739  prmgaplem5  15740  prmgaplem6  15741  ismre  16231  mrcflem  16247  mrcval  16251  ismri  16272  isacs  16293  isacs1i  16299  catlid  16325  catrid  16326  ismon  16374  isnat  16588  eldmcoa  16696  coaval  16699  fncnvimaeqv  16741  lubeldm  16962  glbeldm  16975  gsumress  17257  gsumval2  17261  ismhm  17318  issubm  17328  issubmd  17330  mhmeql  17345  mrcmndind  17347  grplinv  17449  issubg  17575  cycsubg  17603  isnsg  17604  ghmeql  17664  isgim  17685  isga  17705  elcntz  17736  elcntzsn  17739  symgfix2  17817  pmtrval  17852  pmtrrn  17858  symgsssg  17868  symgfisg  17869  psgnunilem5  17895  odid  17938  odlem2  17939  gexid  17977  gexlem2  17978  gexdvds  17980  isslw  18004  pgpssslw  18010  pj1id  18093  efgsfo  18133  oddvdssubg  18239  dprdwd  18391  pgpfac1lem5  18459  ablfaclem2  18466  isirred  18680  isrim0  18704  issubrg  18761  isabv  18800  islss  18916  islmhm  19008  lmhmeql  19036  islmim  19043  islbs  19057  gsumbagdiaglem  19356  psrmulcllem  19368  psrlidm  19384  psrridm  19385  psrass1  19386  psrcom  19390  mplsubglem  19415  mpllsslem  19416  mplmonmul  19445  evlsval2  19501  coe1fsupp  19565  coe1ae0  19567  coe1mul2  19620  zrhcofipsgn  19920  psgndiflemB  19927  elocv  19993  isobs  20045  dsmmelbas  20064  frlmelbas  20081  frlmssuvc2  20115  islinds  20129  dmatel  20280  dmatmulcl  20287  scmatel  20292  scmateALT  20299  symgmatr01lem  20440  pmatcoe1fsupp  20487  cpmatel  20497  chpscmat  20628  istopon  20698  fctop  20789  cctop  20791  ppttop  20792  pptbas  20793  epttop  20794  iscld  20812  clscld  20832  isnei  20888  neips  20898  neiptopnei  20917  iscn  21020  iscnp  21022  ordthauslem  21168  cmpsublem  21183  conncompconn  21216  2ndc1stc  21235  2ndcdisj  21240  locfincmp  21310  elkgen  21320  xkoopn  21373  xkoccn  21403  txdis1cn  21419  pthaus  21422  txkgen  21436  xkohaus  21437  xkococnlem  21443  xkococn  21444  xkoinjcn  21471  txconn  21473  elqtop  21481  nrmr0reg  21533  elmptrab  21611  fbssfi  21622  opnfbas  21627  elfg  21656  cfinfil  21678  csdfil  21679  supfil  21680  filssufilg  21696  uffix  21706  fixufil  21707  uffixfr  21708  uffixsn  21710  ufinffr  21714  ufilen  21715  elflim2  21749  supnfcls  21805  fclscf  21810  flimfnfcls  21813  alexsubALTlem2  21833  alexsubALTlem4  21835  alexsubALT  21836  ptcmplem2  21838  tmdgsum2  21881  symgtgp  21886  ghmcnp  21899  elutop  22018  isucn  22063  iscfilu  22073  ispsmet  22090  ismet  22109  isxmet  22110  elblps  22173  elbl  22174  restmetu  22356  icccmp  22609  elcncf  22673  ishtpy  22752  isphtpy  22761  om1elbas  22813  iscfil  23044  iscau  23055  iscmet  23063  lmle  23080  rrxfsupp  23166  minveclem3  23181  minveclem4  23184  ovolshftlem1  23258  ovolscalem1  23262  ovolicc2lem3  23268  iundisj  23297  dyadmax  23347  dyadmbllem  23348  opnmbllem  23350  vitalilem2  23359  vitalilem3  23360  elcpn  23678  ig1pval3  23915  coelem  23963  quotlem  24036  elqaalem1  24055  elqaalem3  24057  aannenlem1  24064  aannenlem2  24065  aalioulem2  24069  radcnv0  24151  dmarea  24665  jensen  24696  ftalem4  24783  ftalem5  24784  efnnfsumcl  24810  efchtdvds  24866  sqff1o  24889  fsumdvdsdiaglem  24890  dvdsppwf1o  24893  dvdsflf1o  24894  dvdsflsumcom  24895  musum  24898  muinv  24900  logfac2  24923  dchrelbas  24942  dchrfi  24961  lgsfle1  25012  lgsle1  25018  lgsdirprm  25037  lgsne0  25041  lgsquadlem1  25086  lgsquadlem2  25087  2lgslem1b  25098  dchrvmasumlem1  25165  logsqvma  25212  pntleml  25281  tgellng  25429  mircgr  25533  mirbtwn  25534  iseqlg  25728  ttgelitv  25744  upgrle  25966  upgrbi  25969  umgredg2  25976  umgrbi  25977  upgr1elem  25988  edgupgr  26010  edgumgr  26011  upgredg  26013  numedglnl  26020  edgusgr  26036  usgruspgrb  26057  usgredg2ALT  26066  ushgredgedg  26102  ushgredgedgloop  26104  usgrexmplef  26132  subumgredg2  26158  subupgr  26160  upgrreslem  26177  umgrreslem  26178  upgrres1  26186  nbgrel  26219  nbupgrel  26222  nbumgrvtx  26223  nbusgreledg  26230  nbgrnself  26238  nbusgredgeu0  26251  nbusgrf1o0  26252  uvtxael  26269  uvtxael1  26277  uvtxusgrel  26285  1hevtxdg1  26383  umgr2v2e  26402  vtxdgoddnumeven  26430  rgrusgrprc  26466  rgrx0ndm  26470  lfgrwlkprop  26565  iswwlks  26709  iswwlksn  26711  wwlknon  26723  wspthnon  26724  wwlksn0  26729  wlknwwlksnsur  26757  wlkwwlksur  26764  wwlksnextsur  26776  wlksnwwlknvbij  26784  wwlks2onv  26828  rusgrnumwwlkslem  26845  rusgrnumwwlks  26850  isclwwlks  26861  isclwwlksn  26863  clwwlksvbij  26902  clwwlksnscsh  26920  eleclclwwlksn  26933  clwwlksnun  26954  eupth2lems  27078  konigsberglem4  27097  fusgreg2wsplem  27171  numclwwlkovfel2  27188  numclwwlkovgel  27193  numclwlk1lem2foa  27195  numclwwlk2lem1  27206  numclwlk2lem2f  27207  numclwlk2lem2f1o  27209  grpoidinv2  27339  grpoinv  27349  isssp  27549  islno  27578  isblo  27607  ishmo  27636  ubthlem1  27696  ubthlem2  27697  htthlem  27744  ocel  28110  shsval2i  28216  ococin  28237  chsupsn  28242  eleigvec  28786  cnlnadjlem5  28900  shatomistici  29190  hatomistici  29191  nnindf  29539  ordtconnlem1  29944  indf1ofs  30062  sigagenval  30177  ldsysgenld  30197  ldgenpisyslem1  30200  ldgenpisyslem2  30201  ldgenpisys  30203  ddemeas  30273  ismbfm  30288  imambfm  30298  dya2iocuni  30319  oms0  30333  omssubadd  30336  elcarsg  30341  issibf  30369  sitgfval  30377  oddpwdc  30390  eulerpartlemgh  30414  eulerpartlemgs2  30416  dstfrvel  30509  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemiex  30537  ballotlemfrcn0  30565  ballotlemirc  30567  ballotlem7  30571  reprsum  30665  reprsuc  30667  reprpmtf1o  30678  reprdifc  30679  connpconn  31191  iscvm  31215  cvmsi  31221  cvmsval  31222  cvmliftmolem2  31238  cvmliftiota  31257  snmlval  31287  elmpst  31407  sltval2  31783  sltres  31789  conway  31884  scutcut  31886  scutbday  31887  scutun12  31891  scutbdaybnd  31895  scutbdaylt  31896  lineelsb2  32230  linerflx1  32231  fwddifval  32244  fwddifnval  32245  rankeq1o  32253  finminlem  32287  fneint  32318  fnessref  32327  topmeet  32334  topjoin  32335  neifg  32341  relowlssretop  33182  fin2solem  33366  fin2so  33367  poimirlem4  33384  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem31  33411  poimirlem32  33412  opnmbllem0  33416  mblfinlem2  33418  itg2gt0cn  33436  indexa  33499  nninfnub  33518  istotbnd  33539  sstotbnd2  33544  isbnd  33550  isrngohom  33735  isrngoiso  33748  isidl  33784  ispridl  33804  ismaxidl  33810  prnc  33837  isfldidl  33838  islshp  34085  lssats  34118  islfl  34166  isat  34392  atlatmstc  34425  islln  34611  islpln  34635  islvol  34678  linepsubN  34857  elpmap  34863  pmapsub  34873  elpadd  34904  paddvaln0N  34906  islhp  35101  isldil  35215  isltrn  35224  isdilN  35260  istrnN  35263  diaval  36140  diaelval  36141  diaeldm  36144  diaelrnN  36153  cdlemm10N  36226  docaclN  36232  dibglbN  36274  dicval  36284  dicfnN  36291  dicvalrelN  36293  dihglblem2aN  36401  dihglblem2N  36402  dihglblem3N  36403  dih1dimatlem  36437  dihglb2  36450  dochvalr  36465  doch2val2  36472  dochocss  36474  islpolN  36591  mapd0  36773  isnacs  37086  elmzpcl  37108  mzpindd  37128  rencldnfilem  37203  irrapxlem6  37210  pellexlem3  37214  pellexlem5  37216  elpell1qr  37230  elpell14qr  37232  elpell1234qr  37234  pellfundre  37264  pellfundge  37265  pellfundlb  37267  pellfundglb  37268  rmspecnonsq  37291  jm2.22  37381  jm2.23  37382  rpnnen3lem  37417  fnwe2lem2  37440  fnwe2lem3  37441  elmnc  37525  dgraalem  37534  dgraaub  37537  mpaalem  37541  rgspnmin  37560  issdrg  37586  rfovcnvf1od  38118  nzss  38336  iccshift  39547  iooshift  39551  limcperiod  39660  sumnnodd  39662  ioodvbdlimc1lem1  39909  dvnprodlem1  39924  dvnprodlem3  39926  itgperiod  39960  stoweidlem14  39994  stoweidlem15  39995  stoweidlem16  39996  stoweidlem31  40011  stoweidlem36  40016  stoweidlem46  40026  stoweidlem48  40028  fourierdlem2  40089  fourierdlem3  40090  fourierdlem20  40107  fourierdlem25  40112  fourierdlem37  40124  fourierdlem42  40129  fourierdlem48  40134  fourierdlem51  40137  fourierdlem63  40149  fourierdlem64  40150  fourierdlem65  40151  fourierdlem79  40165  fourierdlem81  40167  elaa2lem  40213  etransclem24  40238  etransclem26  40240  etransclem28  40242  etransclem35  40249  etransclem48  40262  salgenval  40304  salgenn0  40312  salgencl  40313  sssalgen  40316  salgenss  40317  salgenuni  40318  issalgend  40319  salgencntex  40324  subsaliuncllem  40338  sge0fodjrnlem  40396  meadjiunlem  40445  caragenel  40472  ovnlecvr  40535  ovnpnfelsup  40536  ovncvrrp  40541  ovnsubaddlem1  40547  hoidmv1lelem1  40568  hoidmv1lelem2  40569  hoidmv1lelem3  40570  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem4  40575  ovnhoilem1  40578  ovnlecvr2  40587  ovncvr2  40588  issmflem  40699  smflimlem2  40743  smflimlem3  40744  smflimsuplem2  40790  iccpart  41116  dfodd2  41314  dfeven5  41343  dfodd7  41344  1hegrlfgr  41478  sprel  41499  prelspr  41501  sprsymrelfolem2  41508  sprsymrelf  41510  ismgmhm  41548  issubmgm  41554  rabsubmgmd  41556  mgmhmeql  41568  assintop  41610  isassintop  41611  assintopcllaw  41613  isrnghm  41657  isrngisom  41661  0even  41696  2even  41698  2zrngamgm  41704  dmatALTbasel  41956  lcoval  41966  elbigo  42110  secval  42253  cscval  42254  cotval  42255
  Copyright terms: Public domain W3C validator