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

Theorem elrab 3326
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 2746 . 2 𝑥𝐴
2 nfcv 2746 . 2 𝑥𝐵
3 nfv 1828 . 2 𝑥𝜓
4 elrab.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
51, 2, 3, 4elrabf 3324 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  {crab 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170
This theorem is referenced by:  elrab3  3327  elrab2  3328  ralrab  3330  rexrab  3332  rabsnt  4205  unimax  4399  ssintub  4420  intminss  4428  rabxfrd  4806  ssimaex  6154  weniso  6478  canth  6482  sorpsscmpl  6819  onnminsb  6869  dfom2  6932  ssnlim  6948  elsuppfn  7163  ressuppssdif  7176  oeeulem  7541  nnawordex  7577  elpmg  7732  fineqvlem  8032  mapfienlem2  8167  supub  8221  suplub  8222  ordtypelem6  8284  ordtypelem7  8285  hartogslem1  8303  hartogs  8305  wemapsolem  8311  card2on  8315  elharval  8324  wdom2d  8341  cantnfs  8419  oemapvali  8437  rankuni2b  8572  scottex  8604  tskwe  8632  cardid2  8635  iscard2  8658  harval2  8679  cardmin2  8680  acni3  8726  alephsuc2  8759  kmlem1  8828  cofsmo  8947  coftr  8951  fin23lem11  8995  enfin2i  8999  fin1a2lem9  9086  fin1a2lem11  9088  axcc4  9117  axdc3lem2  9129  zorn2lem7  9180  ondomon  9237  alephval2  9246  grutsk  9496  pinq  9601  negf1o  10307  fiminre  10817  infm3  10827  nnind  10881  peano2uz2  11293  peano5uzi  11294  dfuzi  11296  uzind  11297  uzind3  11299  eluz1  11519  uzind4  11574  nnwos  11583  eqreznegel  11602  zsupss  11605  zmin  11612  elixx1  12007  elioo2  12039  elfz1  12153  flval3  12429  serge0  12668  expge0  12709  expge1  12710  hashbclem  13041  pr2pwpr  13062  elss2prb  13069  hash2sspr  13070  elss2prOLD  13071  wrdmap  13133  wwlktovfo  13491  shftf  13609  rlimrege0  14100  incexc2  14351  dvdsdivcl  14818  divalglem4  14899  divalgmod  14909  divalgmodOLD  14910  bitsval  14926  bezout  15040  dfgcd2  15043  lcmledvds  15092  lcmgcdlem  15099  lcmfledvds  15125  1nprm  15172  1idssfct  15173  isprm2  15175  phicl2  15253  hashdvds  15260  phisum  15275  odzval  15276  odzcllem  15277  odzdvds  15280  pcpremul  15328  prmreclem1  15400  prmreclem2  15401  prmreclem3  15402  prmreclem5  15404  ramub  15497  rami  15499  ramub1lem1  15510  ramub1lem2  15511  prmgaplem3  15537  prmgaplem4  15538  prmgaplem5  15539  prmgaplem6  15540  ismre  16015  mrcflem  16031  mrcval  16035  ismri  16056  isacs  16077  isacs1i  16083  catlid  16109  catrid  16110  ismon  16158  isnat  16372  eldmcoa  16480  coaval  16483  fncnvimaeqv  16525  lubeldm  16746  glbeldm  16759  gsumress  17041  gsumval2  17045  ismhm  17102  issubm  17112  issubmd  17114  mhmeql  17129  mrcmndind  17131  grplinv  17233  issubg  17359  cycsubg  17387  isnsg  17388  ghmeql  17448  isgim  17469  isga  17489  elcntz  17520  elcntzsn  17523  symgfix2  17601  pmtrval  17636  pmtrrn  17642  symgsssg  17652  symgfisg  17653  psgnunilem5  17679  odid  17722  odlem2  17723  gexid  17761  gexlem2  17762  gexdvds  17764  isslw  17788  pgpssslw  17794  pj1id  17877  efgsfo  17917  oddvdssubg  18023  dprdwd  18175  pgpfac1lem5  18243  ablfaclem2  18250  isirred  18464  isrim0  18488  issubrg  18545  isabv  18584  islss  18698  islmhm  18790  lmhmeql  18818  islmim  18825  islbs  18839  gsumbagdiaglem  19138  psrmulcllem  19150  psrlidm  19166  psrridm  19167  psrass1  19168  psrcom  19172  mplsubglem  19197  mpllsslem  19198  mplmonmul  19227  evlsval2  19283  coe1fsupp  19347  coe1ae0  19349  coe1mul2  19402  zrhcofipsgn  19699  psgndiflemB  19706  elocv  19769  isobs  19821  dsmmelbas  19840  frlmelbas  19857  frlmssuvc2  19891  islinds  19905  dmatel  20056  dmatmulcl  20063  scmatel  20068  scmateALT  20075  symgmatr01lem  20216  pmatcoe1fsupp  20263  cpmatel  20273  chpscmat  20404  istopon  20478  fctop  20556  cctop  20558  ppttop  20559  pptbas  20560  epttop  20561  iscld  20579  clscld  20599  isnei  20655  neips  20665  neiptopnei  20684  iscn  20787  iscnp  20789  ordthauslem  20935  cmpsublem  20950  concompcon  20983  2ndc1stc  21002  2ndcdisj  21007  locfincmp  21077  elkgen  21087  xkoopn  21140  xkoccn  21170  txdis1cn  21186  pthaus  21189  txkgen  21203  xkohaus  21204  xkococnlem  21210  xkococn  21211  xkoinjcn  21238  txcon  21240  elqtop  21248  nrmr0reg  21300  elmptrab  21378  fbssfi  21389  opnfbas  21394  elfg  21423  cfinfil  21445  csdfil  21446  supfil  21447  filssufilg  21463  uffix  21473  fixufil  21474  uffixfr  21475  uffixsn  21477  ufinffr  21481  ufilen  21482  elflim2  21516  supnfcls  21572  fclscf  21577  flimfnfcls  21580  alexsubALTlem2  21600  alexsubALTlem4  21602  alexsubALT  21603  ptcmplem2  21605  tmdgsum2  21648  symgtgp  21653  ghmcnp  21666  elutop  21785  isucn  21830  iscfilu  21840  ispsmet  21857  ismet  21875  isxmet  21876  elblps  21939  elbl  21940  restmetu  22122  icccmp  22364  elcncf  22427  ishtpy  22506  isphtpy  22515  om1elbas  22567  iscfil  22785  iscau  22796  iscmet  22804  lmle  22821  rrxfsupp  22906  minveclem3  22921  minveclem4  22924  ovolshftlem1  22997  ovolscalem1  23001  ovolicc2lem3  23007  iundisj  23036  dyadmax  23085  dyadmbllem  23086  opnmbllem  23088  vitalilem2  23097  vitalilem3  23098  elcpn  23416  ig1pval3  23651  coelem  23699  quotlem  23772  elqaalem1  23791  elqaalem3  23793  aannenlem1  23800  aannenlem2  23801  aalioulem2  23805  radcnv0  23887  dmarea  24397  jensen  24428  ftalem4  24515  ftalem5  24516  efnnfsumcl  24542  efchtdvds  24598  sqff1o  24621  fsumdvdsdiaglem  24622  dvdsppwf1o  24625  dvdsflf1o  24626  dvdsflsumcom  24627  musum  24630  muinv  24632  logfac2  24655  dchrelbas  24674  dchrfi  24693  lgsfle1  24744  lgsle1  24750  lgsdirprm  24769  lgsne0  24773  lgsquadlem1  24818  lgsquadlem2  24819  2lgslem1b  24830  dchrvmasumlem1  24897  logsqvma  24944  pntleml  25013  tgellng  25162  mircgr  25266  mirbtwn  25267  iseqlg  25461  ttgelitv  25477  umgrale  25612  umgra1  25617  edg  25644  uslgra1  25663  usgra1  25664  usgraedg2  25666  usgraedgrnv  25668  usgrarnedg  25675  usgraedg4  25678  usgraexmplef  25691  usgrares1  25701  nbgrael  25717  nbgraeledg  25721  nbgraf1olem3  25734  cusgrarn  25750  nbcusgra  25754  cusgrares  25763  uvtxel  25779  uvtxnbgra  25783  cusgrauvtxb  25786  iswwlk  25973  iswwlkn  25974  wlknwwlknsur  26002  wlkiswwlksur  26009  wwlkextsur  26021  wlknwwlknvbij  26030  isclwwlk  26058  isclwwlkn  26059  clwwlkprop  26060  clwwlknprop  26062  clwwlkvbij  26091  clwwlknscsh  26109  eleclclwwlkn  26122  el2wlkonot  26158  el2spthonot  26159  el2spthonot0  26160  el2wlksoton  26167  el2spthsoton  26168  el2wlksotot  26171  rusgranumwlklem0  26237  rusgranumwlklem1  26238  rusgranumwlklem3  26240  rusgranumwlks  26245  eupath2  26269  umgrabi  26272  konigsberg  26276  2spotdisj  26350  usg2spot2nb  26354  usgreg2spot  26356  numclwwlkun  26368  numclwwlkovfel2  26372  numclwwlkovgel  26377  numclwlk1lem2foa  26380  numclwwlk2lem1  26391  numclwlk2lem2f  26392  numclwlk2lem2f1o  26394  grpoidinv2  26515  grpoinv  26525  isssp  26763  islno  26794  isblo  26823  ishmo  26852  ubthlem1  26912  ubthlem2  26913  htthlem  26960  ocel  27326  shsval2i  27432  ococin  27453  chsupsn  27458  eleigvec  28002  cnlnadjlem5  28116  shatomistici  28406  hatomistici  28407  nnindf  28754  ordtconlem1  29100  indf1ofs  29217  sigagenval  29332  ldsysgenld  29352  ldgenpisyslem1  29355  ldgenpisyslem2  29356  ldgenpisys  29358  ddemeas  29428  ismbfm  29443  imambfm  29453  dya2iocuni  29474  oms0  29488  omssubadd  29491  elcarsg  29496  issibf  29524  sitgfval  29532  oddpwdc  29545  eulerpartlemgh  29569  eulerpartlemgs2  29571  dstfrvel  29664  ballotlemfc0  29683  ballotlemfcc  29684  ballotlemiex  29692  ballotlemfrcn0  29720  ballotlemirc  29722  ballotlem7  29726  conpcon  30273  iscvm  30297  cvmsi  30303  cvmsval  30304  cvmliftmolem2  30320  cvmliftiota  30339  snmlval  30369  elmpst  30489  sltval2  30855  sltres  30863  nodenselem7  30888  nofulllem5  30907  lineelsb2  31227  linerflx1  31228  fwddifval  31241  fwddifnval  31242  rankeq1o  31250  finminlem  31284  fneint  31315  fnessref  31324  topmeet  31331  topjoin  31332  neifg  31338  relowlssretop  32186  fin2solem  32364  fin2so  32365  poimirlem4  32382  poimirlem25  32403  poimirlem26  32404  poimirlem27  32405  poimirlem31  32409  poimirlem32  32410  opnmbllem0  32414  mblfinlem2  32416  itg2gt0cn  32434  indexa  32497  nninfnub  32516  istotbnd  32537  sstotbnd2  32542  isbnd  32548  isrngohom  32733  isrngoiso  32746  isidl  32782  ispridl  32802  ismaxidl  32808  prnc  32835  isfldidl  32836  islshp  33083  lssats  33116  islfl  33164  isat  33390  atlatmstc  33423  islln  33609  islpln  33633  islvol  33676  linepsubN  33855  elpmap  33861  pmapsub  33871  elpadd  33902  paddvaln0N  33904  islhp  34099  isldil  34213  isltrn  34222  isdilN  34258  istrnN  34261  diaval  35138  diaelval  35139  diaeldm  35142  diaelrnN  35151  cdlemm10N  35224  docaclN  35230  dibglbN  35272  dicval  35282  dicfnN  35289  dicvalrelN  35291  dihglblem2aN  35399  dihglblem2N  35400  dihglblem3N  35401  dih1dimatlem  35435  dihglb2  35448  dochvalr  35463  doch2val2  35470  dochocss  35472  islpolN  35589  mapd0  35771  isnacs  36084  elmzpcl  36106  mzpindd  36126  rencldnfilem  36201  irrapxlem6  36208  pellexlem3  36212  pellexlem5  36214  elpell1qr  36228  elpell14qr  36230  elpell1234qr  36232  pellfundre  36262  pellfundge  36263  pellfundlb  36265  pellfundglb  36266  rmspecnonsq  36289  jm2.22  36379  jm2.23  36380  rpnnen3lem  36415  fnwe2lem2  36438  fnwe2lem3  36439  elmnc  36524  dgraalem  36533  dgraaub  36536  mpaalem  36540  rgspnmin  36559  issdrg  36585  rfovcnvf1od  37117  nzss  37337  iccshift  38391  iooshift  38395  limcperiod  38495  sumnnodd  38497  ioodvbdlimc1lem1  38621  dvnprodlem1  38636  dvnprodlem3  38638  itgperiod  38673  stoweidlem14  38707  stoweidlem15  38708  stoweidlem16  38709  stoweidlem31  38724  stoweidlem36  38729  stoweidlem46  38739  stoweidlem48  38741  fourierdlem2  38802  fourierdlem3  38803  fourierdlem20  38820  fourierdlem25  38825  fourierdlem37  38837  fourierdlem42  38842  fourierdlem48  38847  fourierdlem51  38850  fourierdlem63  38862  fourierdlem64  38863  fourierdlem65  38864  fourierdlem79  38878  fourierdlem81  38880  elaa2lem  38926  etransclem24  38951  etransclem26  38953  etransclem28  38955  etransclem35  38962  etransclem48  38975  salgenval  39017  salgenn0  39025  salgencl  39026  sssalgen  39029  salgenss  39030  salgenuni  39031  issalgend  39032  salgencntex  39037  subsaliuncllem  39051  sge0fodjrnlem  39109  meadjiunlem  39158  caragenel  39185  ovnlecvr  39248  ovnpnfelsup  39249  ovncvrrp  39254  ovnsubaddlem1  39260  hoidmv1lelem1  39281  hoidmv1lelem2  39282  hoidmv1lelem3  39283  hoidmvlelem1  39285  hoidmvlelem2  39286  hoidmvlelem4  39288  ovnhoilem1  39291  ovnlecvr2  39300  ovncvr2  39301  issmflem  39413  smflimlem2  39458  smflimlem3  39459  iccpart  39755  iseven  39880  isodd  39881  dfodd2  39888  dfeven5  39917  dfodd7  39918  upgrle  40314  upgrbi  40317  umgredg2  40323  umgrbi  40324  upgr1elem  40335  edgupgr  40365  edgumgr  40366  upgredg  40368  edgusgr  40389  usgruspgrb  40409  usgredg2ALT  40418  ushgredgedga  40454  ushgredgedgaloop  40456  subumgredg2  40507  subupgr  40509  upgrres1  40530  nbgrel  40562  nbupgrel  40565  nbumgrvtx  40566  nbusgreledg  40573  nbgrnself  40581  nbusgredgeu0  40594  nbusgrf1o0  40595  uvtxael  40612  uvtxael1  40620  uvtxusgrel  40628  1hevtxdg1  40719  1hegrlfgr  40720  umgr2v2e  40739  rgrusgrprc  40787  rgrx0ndm  40791  lfgrwlkprop  40894  iswwlks  41037  iswwlksn  41039  wwlknon  41051  wspthnon  41052  wwlksn0  41057  wlknwwlksnsur  41085  wlkwwlksur  41092  wwlksnextsur  41104  wlksnwwlknvbij  41112  wwlks2onv  41156  rusgrnumwwlks  41175  isclwwlks  41186  isclwwlksn  41188  clwwlksvbij  41227  clwwlksnscsh  41245  eleclclwwlksn  41258  clwwlksnun  41279  eupth2lems  41404  konigsberglem4  41423  fusgr2wsp2nb  41496  fusgreg2wsp  41498  2wspmdisj  41499  av-numclwwlkovfel2  41512  av-numclwwlkovgel  41517  av-numclwlk1lem2foa  41519  av-numclwwlk2lem1  41530  av-numclwlk2lem2f  41531  av-numclwlk2lem2f1o  41533  ismgmhm  41571  issubmgm  41577  rabsubmgmd  41579  mgmhmeql  41591  assintop  41633  isassintop  41634  assintopcllaw  41636  isrnghm  41680  isrngisom  41684  0even  41719  2even  41721  2zrngamgm  41727  dmatALTbasel  41983  lcoval  41993  elbigo  42141  secval  42246  cscval  42247  cotval  42248
  Copyright terms: Public domain W3C validator