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

Theorem elrab2 3516
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1 (𝑥 = 𝐴 → (𝜑𝜓))
elrab2.2 𝐶 = {𝑥𝐵𝜑}
Assertion
Ref Expression
elrab2 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3 𝐶 = {𝑥𝐵𝜑}
21eleq2i 2841 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 3513 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 264 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wcel 2144  {crab 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rab 3069  df-v 3351
This theorem is referenced by:  elrabsf  3624  pwnss  4958  fvmpti  6423  fvmptss2  6446  tfis  7200  elom  7214  oawordeulem  7787  oeeulem  7834  mapfienlem1  8465  mapfienlem3  8467  mapfien  8468  ordtypelem2  8579  ordtypelem3  8580  ordtypelem9  8586  wemapso2lem  8612  inf3lema  8684  oemapvali  8744  tz9.12lem3  8815  cofsmo  9292  enfin2i  9344  fin23lem28  9363  isf32lem6  9381  hsmexlem4  9452  zorn2lem2  9520  pwfseqlem1  9681  pwfseqlem3  9683  nqereu  9952  elz  11580  zsupss  11979  rpnnen1lem5  12020  rpnnen1lem5OLD  12026  elrp  12036  repos  12475  wwlktovf  13908  wwlktovf1  13909  wwlktovfo  13910  sqrlem1  14190  sqrlem2  14191  sqrlem6  14195  sqrlem7  14196  ello1  14453  elo1  14464  rlimrege0  14517  divalglem2  15325  divalglem4  15326  divalglem5  15327  divalglem9  15331  divalglem10  15332  bitsfzolem  15363  gcdcllem1  15428  gcdcllem2  15429  gcdcllem3  15430  bezoutlem1  15463  bezoutlem3  15465  bezoutlem4  15466  isprm  15593  maxprmfct  15627  phimullem  15690  eulerthlem1  15692  eulerthlem2  15693  hashgcdlem  15699  pclem  15749  pcprecl  15750  pcprendvds  15751  infpn2  15823  prmreclem1  15826  prmreclem2  15827  prmreclem3  15828  prmreclem5  15830  1arith  15837  elgz  15841  4sqlem13  15867  4sqlem17  15871  4sqlem18  15872  vdwnnlem2  15906  vdwnnlem3  15907  ramtlecl  15910  isdrs  17141  istos  17242  islat  17254  isclat  17316  isdlat  17400  istsr  17424  issgrp  17492  ismnddef  17503  gsumvallem2  17579  isgrp  17635  elnmz  17840  gastacl  17948  gastacos  17949  symgfixelq  18059  psgneldm  18129  sylow1lem2  18220  sylow1lem4  18222  sylow2alem1  18238  sylow2alem2  18239  efgsdm  18349  iscmn  18406  iscyg  18487  iscyggen  18488  dprdw  18616  ablfacrplem  18671  ablfacrp  18672  ablfac1c  18677  ablfac1eu  18679  pgpfaclem1  18687  ablfaclem3  18693  ablfac2  18695  issrg  18714  isring  18758  iscrng  18761  isdrng  18960  islmod  19076  islvec  19316  lspsolvlem  19355  lbsextlem1  19372  lbsextlem3  19374  lbsextlem4  19375  islpir  19463  isnzr  19473  isrrg  19502  isdomn  19508  isassa  19529  psrbag  19578  psrbaglefi  19586  psrbagconcl  19587  psrbagconf1o  19588  gsumbagdiaglem  19589  mplelbas  19644  isphl  20189  pjdm  20267  ishil  20278  frlmssuvc1  20349  frlmssuvc2  20350  frlmsslsp  20351  gsummatr01lem1  20679  gsummatr01lem4  20682  gsummatr01  20683  mretopd  21116  neipeltop  21153  isperf  21175  ist0  21344  ist1  21345  ishaus  21346  iscnrm  21347  isreg  21356  isnrm  21359  ispnrm  21363  iscmp  21411  hauscmplem  21429  isconn  21436  conncompss  21456  is1stc  21464  islly  21491  isnlly  21492  dfac14lem  21640  ishmeo  21782  ptcmplem3  22077  ptcmplem4  22078  istmd  22097  istgp  22100  tgpconncompeqg  22134  tgpt0  22141  qustgpopn  22142  istrg  22186  istdrg  22188  istlm  22207  istvc  22214  iscusp  22322  imasdsf1olem  22397  isxms  22471  isms  22473  blcld  22529  prdsxmslem2  22553  isngp  22619  isnrg  22683  isnlm  22698  icccmplem1  22844  icccmplem2  22845  isclm  23082  iscph  23188  isbn  23353  iscms  23360  ivthlem1  23438  ivthlem2  23439  ivthlem3  23440  elovolm  23462  ovolicc2lem2  23505  ovolicc2lem4  23507  ovolicc2lem5  23508  ismbl  23513  dyadmbllem  23586  dyadmbl  23587  ismbf1  23611  isi1f  23660  isibl  23751  isuc1p  24119  ismon1p  24121  radcnvle  24393  abelthlem2  24405  abelthlem7a  24410  atans  24877  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamgulmlem5  24979  lgambdd  24983  wilthlem2  25015  wilthlem3  25016  ftalem3  25021  sqff1o  25128  dvdsmulf1o  25140  lgslem2  25243  lgslem3  25244  lgsfcl2  25248  rpvmasumlem  25396  dchrvmaeq0  25413  dchrisum0re  25422  pntlem3  25518  axcontlem2  26065  lfgredgge2  26239  uspgredg2vlem  26336  uspgredg2v  26337  usgredg2vlem1  26338  usgredg2vlem2  26339  ushgredgedg  26342  ushgredgedgloop  26344  ushgredgedgloopOLD  26345  uhgrspan1  26417  upgrreslem  26418  umgrreslem  26419  isfusgr  26432  nbupgrres  26487  nbusgredgeu0  26492  nbusgrf1o0  26493  uvtxel  26513  uvtxel1  26523  cusgrexilem2  26572  cusgrfilem2  26586  vtxdginducedm1lem4  26672  iswspthn  26977  wwlknon  26987  wspthnon  26988  wspthnonOLD  26990  wlknwwlksnfun  27021  wlknwwlksninj  27022  wlkwwlkfun  27028  wlkwwlkinj  27029  wlkwwlksur  27030  wwlksnextfun  27040  wwlksnextinj  27041  wwlksnextsur  27042  wwlksnextproplem3  27053  clwlkclwwlkflem  27151  clwlkclwwlkfolem  27154  isclwwlkn  27177  clwwlkel  27199  clwwlkf  27200  clwwlkf1  27202  clwlksfclwwlk1hashnOLD  27237  clwlksfoclwwlkOLD  27241  clwlksf1clwwlklem0OLD  27242  isclwwlknon  27261  frgrwopreglem3  27493  frgrwopreglem5lem  27499  frgrwopreglem5  27500  isablo  27734  iscbn  28054  hcau  28375  issh  28399  isch  28413  elcnop  29050  ellnop  29051  elbdop  29053  elhmop  29066  elcnfn  29075  ellnfn  29076  isst  29406  ishst  29407  ela  29532  isomnd  30035  isslmd  30089  isorng  30133  iscref  30245  isrrext  30378  ispisys  30549  isldsys  30553  isros  30565  issros  30572  oddpwdc  30750  eulerpartleme  30759  eulerpartlemo  30761  eulerpartlemd  30762  eulerpartlemt0  30765  eulerpartlemf  30766  eulerpartlemt  30767  eulerpartlemr  30770  eulerpartlemmf  30771  eulerpartlemgvv  30772  eulerpartlemgs2  30776  eulerpartlemn  30777  elprob  30805  ballotlemelo  30883  ballotleme  30892  bnj1152  31398  bnj1280  31420  subfacp1lem3  31496  subfacp1lem5  31498  erdszelem1  31505  ispconn  31537  issconn  31540  cvmsiota  31591  cvmlift2lem12  31628  rdgprc0  32029  elwlim  32099  neibastop1  32685  neibastop2lem  32686  neibastop2  32687  topdifinffinlem  33525  poimirlem5  33740  poimirlem6  33741  poimirlem7  33742  poimirlem8  33743  poimirlem10  33745  poimirlem11  33746  poimirlem12  33747  poimirlem15  33750  poimirlem16  33751  poimirlem17  33752  poimirlem18  33753  poimirlem19  33754  poimirlem20  33755  poimirlem21  33756  poimirlem22  33757  isprrngo  34174  rabeqel  34355  toycom  34775  isopos  34982  isoml  35040  isatl  35101  iscvlat  35125  ishlat1  35154  cdlemm10N  36921  dihglblem2N  37097  lcfl1lem  37294  lcfls1lem  37337  mapdordlem1a  37437  mapdordlem1  37439  pellqrex  37962  islnm  38166  pwssplit4  38178  islnr  38200  fnlimcnv  40411  stoweidlem14  40742  stoweidlem16  40744  stoweidlem37  40765  stoweidlem48  40776  stoweidlem51  40779  stoweidlem59  40787  salexct  41063  salexct2  41068  salexct3  41071  salgencntex  41072  salgensscntex  41073  ovn0lem  41293  opnvonmbllem1  41360  ovolval5lem2  41381  pimincfltioc  41440  pimdecfgtioo  41441  pimincfltioo  41442  smfresal  41509  smfmullem2  41513  smfpimbor1lem1  41519  smfpimbor1lem2  41520  smfinflem  41537  iseven  42059  isodd  42060  m1expevenALTV  42078  iseven2  42082  isodd3  42083  odd2np1ALTV  42103  opoeALTV  42112  opeoALTV  42113  isgbe  42157  isgbow  42158  isgbo  42159  sprsymrelfo  42265  0nodd  42328  1odd  42329  2nodd  42330  iscmgmALT  42378  issgrpALT  42379  iscsgrpALT  42380  isrng  42394  1neven  42450  2zlidl  42452  2zrngamgm  42457  2zrngagrp  42461  2zrngmmgm  42464  2zrngnmrid  42468
  Copyright terms: Public domain W3C validator