Theorem elrab2 3621

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

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2874	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3618	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 276	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  {crab 3109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439

This theorem is referenced by:  rru  3704  elrabsf  3745  fvmpti  6634  fvmptss2  6659  tfis  7425  elom  7439  oawordeulem  8030  oeeulem  8077  mapfienlem1  8714  mapfienlem3  8716  mapfien  8717  ordtypelem2  8829  ordtypelem3  8830  ordtypelem9  8836  wemapso2lem  8862  inf3lema  8933  oemapvali  8993  tz9.12lem3  9064  cofsmo  9537  enfin2i  9589  fin23lem28  9608  isf32lem6  9626  hsmexlem4  9697  zorn2lem2  9765  pwfseqlem1  9926  pwfseqlem3  9928  nqereu  10197  elz  11831  zsupss  12186  rpnnen1lem5  12230  elrp  12241  repos  12684  wwlktovf  14154  wwlktovf1  14155  wwlktovfo  14156  sqrlem1  14436  sqrlem2  14437  sqrlem6  14441  sqrlem7  14442  ello1  14706  elo1  14717  rlimrege0  14770  divalglem2  15579  divalglem4  15580  divalglem5  15581  divalglem9  15585  divalglem10  15586  bitsfzolem  15616  gcdcllem1  15681  gcdcllem2  15682  gcdcllem3  15683  bezoutlem1  15716  bezoutlem3  15718  bezoutlem4  15719  isprm  15846  maxprmfct  15882  phimullem  15945  eulerthlem1  15947  eulerthlem2  15948  hashgcdlem  15954  pclem  16004  pcprecl  16005  pcprendvds  16006  infpn2  16078  prmreclem1  16081  prmreclem2  16082  prmreclem3  16083  prmreclem5  16085  1arith  16092  elgz  16096  4sqlem13  16122  4sqlem17  16126  4sqlem18  16127  vdwnnlem2  16161  vdwnnlem3  16162  ramtlecl  16165  isdrs  17373  istos  17474  islat  17486  isclat  17548  isdlat  17632  istsr  17656  issgrp  17724  ismnddef  17735  gsumvallem2  17811  isgrp  17867  elnmz  18072  gastacl  18180  gastacos  18181  symgfixelq  18292  psgneldm  18362  sylow1lem2  18454  sylow1lem4  18456  sylow2alem1  18472  sylow2alem2  18473  efgsdm  18583  iscmn  18640  iscyg  18721  iscyggen  18722  dprdw  18849  ablfacrplem  18904  ablfacrp  18905  ablfac1c  18910  ablfac1eu  18912  pgpfaclem1  18920  ablfaclem3  18926  ablfac2  18928  issrg  18947  isring  18991  iscrng  18994  isdrng  19196  islmod  19328  islvec  19566  lspsolvlem  19604  lbsextlem1  19620  lbsextlem3  19622  lbsextlem4  19623  islpir  19711  isnzr  19721  isrrg  19750  isdomn  19756  isassa  19777  psrbag  19832  psrbaglefi  19840  psrbagconcl  19841  psrbagconf1o  19842  gsumbagdiaglem  19843  mplelbas  19898  isphl  20454  pjdm  20533  ishil  20544  frlmssuvc1  20620  frlmssuvc2  20621  frlmsslsp  20622  gsummatr01lem1  20948  gsummatr01lem4  20951  gsummatr01  20952  mretopd  21384  neipeltop  21421  isperf  21443  ist0  21612  ist1  21613  ishaus  21614  iscnrm  21615  isreg  21624  isnrm  21627  ispnrm  21631  iscmp  21680  hauscmplem  21698  isconn  21705  conncompss  21725  is1stc  21733  islly  21760  isnlly  21761  dfac14lem  21909  ishmeo  22051  ptcmplem3  22346  ptcmplem4  22347  istmd  22366  istgp  22369  tgpconncompeqg  22403  tgpt0  22410  qustgpopn  22411  istrg  22455  istdrg  22457  istlm  22476  istvc  22483  iscusp  22591  imasdsf1olem  22666  isxms  22740  isms  22742  blcld  22798  prdsxmslem2  22822  isngp  22888  isnrg  22952  isnlm  22967  icccmplem1  23113  icccmplem2  23114  isclm  23351  iscph  23457  isbn  23624  iscms  23631  ivthlem1  23735  ivthlem2  23736  ivthlem3  23737  elovolm  23759  ovolicc2lem2  23802  ovolicc2lem4  23804  ovolicc2lem5  23805  ismbl  23810  dyadmbllem  23883  dyadmbl  23884  ismbf1  23908  isi1f  23958  isibl  24049  isuc1p  24417  ismon1p  24419  radcnvle  24691  abelthlem2  24703  abelthlem7a  24708  atans  25189  lgamgulmlem2  25289  lgamgulmlem3  25290  lgamgulmlem5  25292  lgambdd  25296  wilthlem2  25328  wilthlem3  25329  ftalem3  25334  sqff1o  25441  dvdsmulf1o  25453  lgslem2  25556  lgslem3  25557  lgsfcl2  25561  rpvmasumlem  25745  dchrvmaeq0  25762  dchrisum0re  25771  pntlem3  25867  axcontlem2  26434  lfgredgge2  26592  uspgredg2vlem  26688  uspgredg2v  26689  usgredg2vlem1  26690  usgredg2vlem2  26691  ushgredgedg  26694  ushgredgedgloop  26696  uhgrspan1  26768  upgrreslem  26769  umgrreslem  26770  isfusgr  26783  nbupgrres  26829  nbusgredgeu0  26833  nbusgrf1o0  26834  uvtxel  26853  uvtxel1  26861  cusgrexilem2  26907  cusgrfilem2  26921  vtxdginducedm1lem4  27007  rgrx0ndm  27058  iswspthn  27314  wwlknon  27322  wspthnon  27323  wwlksn0  27328  wwlksnextfun  27363  wwlksnextinj  27364  wwlksnextsurj  27365  wwlksnextproplem3  27377  clwlkclwwlkflem  27469  clwlkclwwlkfolem  27472  isclwwlkn  27492  clwwlkel  27512  clwwlkf  27513  clwwlkf1  27515  isclwwlknon  27557  s2elclwwlknon2  27570  frgrwopreglem3  27785  frgrwopreglem5lem  27791  frgrwopreglem5  27792  isablo  28014  iscbn  28332  hcau  28652  issh  28676  isch  28690  elcnop  29325  ellnop  29326  elbdop  29328  elhmop  29341  elcnfn  29350  ellnfn  29351  isst  29681  ishst  29682  ela  29807  isomnd  30362  isslmd  30468  isorng  30526  iscref  30725  isrrext  30858  ispisys  31028  isldsys  31032  isros  31044  issros  31051  oddpwdc  31229  eulerpartleme  31238  eulerpartlemo  31240  eulerpartlemd  31241  eulerpartlemt0  31244  eulerpartlemf  31245  eulerpartlemt  31246  eulerpartlemr  31249  eulerpartlemmf  31250  eulerpartlemgvv  31251  eulerpartlemgs2  31255  eulerpartlemn  31256  elprob  31284  ballotlemelo  31362  ballotleme  31371  bnj1152  31884  bnj1280  31906  subfacp1lem3  32038  subfacp1lem5  32040  erdszelem1  32047  ispconn  32079  issconn  32082  cvmsiota  32133  cvmlift2lem12  32170  fmla1  32243  gonan0  32248  goaln0  32249  gonar  32251  goalr  32253  sategoelfvb  32275  rdgprc0  32648  elwlim  32720  neibastop1  33317  neibastop2lem  33318  neibastop2  33319  topdifinffinlem  34178  pibp19  34245  pibp21  34246  poimirlem5  34447  poimirlem6  34448  poimirlem7  34449  poimirlem8  34450  poimirlem10  34452  poimirlem11  34453  poimirlem12  34454  poimirlem15  34457  poimirlem16  34458  poimirlem17  34459  poimirlem18  34460  poimirlem19  34461  poimirlem20  34462  poimirlem21  34463  poimirlem22  34464  isprrngo  34879  rabeqel  35067  toycom  35659  isopos  35866  isoml  35924  isatl  35985  iscvlat  36009  ishlat1  36038  cdlemm10N  37804  dihglblem2N  37980  lcfl1lem  38177  lcfls1lem  38220  mapdordlem1a  38320  mapdordlem1  38322  pellqrex  38980  islnm  39181  pwssplit4  39193  islnr  39215  issimpg  40167  fnlimcnv  41509  stoweidlem14  41861  stoweidlem16  41863  stoweidlem37  41884  stoweidlem48  41895  stoweidlem51  41898  stoweidlem59  41906  salexct  42179  salexct2  42184  salexct3  42187  salgencntex  42188  salgensscntex  42189  ovn0lem  42409  opnvonmbllem1  42476  ovolval5lem2  42497  pimincfltioc  42556  pimdecfgtioo  42557  pimincfltioo  42558  smfresal  42625  smfmullem2  42629  smfpimbor1lem1  42635  smfpimbor1lem2  42636  smfinflem  42653  sprsymrelfo  43161  prproropf1olem1  43167  pairreueq  43174  iseven  43295  isodd  43296  m1expevenALTV  43314  iseven2  43318  isodd3  43319  odd2np1ALTV  43341  opoeALTV  43350  opeoALTV  43351  isgbe  43418  isgbow  43419  isgbo  43420  0nodd  43579  1odd  43580  2nodd  43581  iscmgmALT  43629  issgrpALT  43630  iscsgrpALT  43631  isrng  43645  1neven  43701  2zlidl  43703  2zrngamgm  43708  2zrngagrp  43712  2zrngmmgm  43715  2zrngnmrid  43719  itsclc0  44259  itsclc0b  44260