Theorem elrab2 3646

Description: Membership in a restricted 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 2825	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3643	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 275	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439

This theorem is referenced by:  rru  3734  elrabsf  3783  fvmpti  6937  fvmptss2  6964  tfis  7794  elom  7808  oawordeulem  8478  oeeulem  8525  mapfienlem1  9300  mapfienlem3  9302  mapfien  9303  ordtypelem2  9416  ordtypelem3  9417  ordtypelem9  9423  wemapso2lem  9449  inf3lema  9525  oemapvali  9585  tz9.12lem3  9693  cofsmo  10171  enfin2i  10223  fin23lem28  10242  isf32lem6  10260  hsmexlem4  10331  zorn2lem2  10399  pwfseqlem1  10560  pwfseqlem3  10562  nqereu  10831  elz  12481  zsupss  12841  rpnnen1lem5  12885  elrp  12898  repos  13353  wwlktovf  14870  wwlktovf1  14871  wwlktovfo  14872  01sqrexlem1  15156  01sqrexlem2  15157  01sqrexlem6  15161  01sqrexlem7  15162  ello1  15429  elo1  15440  rlimrege0  15493  divalglem2  16313  divalglem4  16314  divalglem5  16315  divalglem9  16319  divalglem10  16320  bitsfzolem  16352  gcdcllem1  16417  gcdcllem2  16418  gcdcllem3  16419  bezoutlem1  16457  bezoutlem3  16459  bezoutlem4  16460  isprm  16591  maxprmfct  16627  phimullem  16697  eulerthlem1  16699  eulerthlem2  16700  hashgcdlem  16706  pclem  16757  pcprecl  16758  pcprendvds  16759  infpn2  16832  prmreclem1  16835  prmreclem2  16836  prmreclem3  16837  prmreclem5  16839  1arith  16846  elgz  16850  4sqlem13  16876  4sqlem17  16880  4sqlem18  16881  vdwnnlem2  16915  vdwnnlem3  16916  ramtlecl  16919  isdrs  18215  istos  18330  islat  18347  isclat  18414  isdlat  18436  istsr  18497  ischn  18521  issgrp  18636  ismnddef  18652  gsumvallem2  18750  isgrp  18860  elnmz  19083  gastacl  19229  gastacos  19230  symgfixelq  19353  psgneldm  19423  sylow1lem2  19519  sylow1lem4  19521  sylow2alem1  19537  sylow2alem2  19538  efgsdm  19650  iscmn  19709  iscyg  19799  iscyggen  19800  dprdw  19932  ablfacrplem  19987  ablfacrp  19988  ablfac1c  19993  ablfac1eu  19995  pgpfaclem1  20003  ablfaclem3  20009  ablfac2  20011  issimpg  20014  isomnd  20043  isrng  20080  issrg  20114  isring  20163  iscrng  20166  isnzr  20438  islring  20464  isrrg  20622  isdomn  20629  isdrng  20657  isorng  20785  islmod  20806  islvec  21047  lspsolvlem  21088  lbsextlem1  21104  lbsextlem3  21106  lbsextlem4  21107  islpir  21274  isphl  21574  pjdm  21653  ishil  21664  frlmssuvc1  21740  frlmssuvc2  21741  frlmsslsp  21742  isassa  21802  psrbag  21864  psrbaglefi  21873  psrbagconcl  21874  psrbagleadd1  21875  gsumbagdiaglem  21877  mplelbas  21937  gsummatr01lem1  22590  gsummatr01lem4  22593  gsummatr01  22594  mretopd  23027  neipeltop  23064  isperf  23086  ist0  23255  ist1  23256  ishaus  23257  iscnrm  23258  isreg  23267  isnrm  23270  ispnrm  23274  iscmp  23323  hauscmplem  23341  isconn  23348  conncompss  23368  is1stc  23376  islly  23403  isnlly  23404  dfac14lem  23552  ishmeo  23694  ptcmplem3  23989  ptcmplem4  23990  istmd  24009  istgp  24012  tgpconncompeqg  24047  tgpt0  24054  qustgpopn  24055  istrg  24099  istdrg  24101  istlm  24120  istvc  24127  iscusp  24233  imasdsf1olem  24308  isxms  24382  isms  24384  blcld  24440  prdsxmslem2  24464  isngp  24531  isnrg  24595  isnlm  24610  icccmplem1  24758  icccmplem2  24759  isclm  25011  iscph  25117  isbn  25285  iscms  25292  ivthlem1  25399  ivthlem2  25400  ivthlem3  25401  elovolm  25423  ovolicc2lem2  25466  ovolicc2lem4  25468  ovolicc2lem5  25469  ismbl  25474  dyadmbllem  25547  dyadmbl  25548  ismbf1  25572  isi1f  25622  isibl  25713  isuc1p  26093  ismon1p  26095  radcnvle  26376  abelthlem2  26389  abelthlem7a  26394  atans  26887  lgamgulmlem2  26987  lgamgulmlem3  26988  lgamgulmlem5  26990  lgambdd  26994  wilthlem2  27026  wilthlem3  27027  ftalem3  27032  sqff1o  27139  mpodvdsmulf1o  27151  dvdsmulf1o  27153  lgslem2  27256  lgslem3  27257  lgsfcl2  27261  rpvmasumlem  27445  dchrvmaeq0  27462  dchrisum0re  27471  pntlem3  27567  elleft  27826  elright  27827  elons  28210  elreno  28417  axcontlem2  28964  lfgredgge2  29123  uspgredg2vlem  29222  uspgredg2v  29223  usgredg2vlem1  29224  usgredg2vlem2  29225  ushgredgedg  29228  ushgredgedgloop  29230  uhgrspan1  29302  upgrreslem  29303  umgrreslem  29304  isfusgr  29317  nbupgrres  29363  nbusgredgeu0  29367  nbusgrf1o0  29368  uvtxel  29387  uvtxel1  29395  cusgrexilem2  29441  cusgrfilem2  29456  vtxdginducedm1lem4  29542  rgrx0ndm  29593  iswspthn  29848  wwlknon  29856  wspthnon  29857  wwlksn0  29862  wwlksnextfun  29897  wwlksnextinj  29898  wwlksnextsurj  29899  wwlksnextproplem3  29910  clwlkclwwlkflem  30005  clwlkclwwlkfolem  30008  isclwwlkn  30028  clwwlkel  30047  clwwlkf  30048  clwwlkf1  30050  isclwwlknon  30092  s2elclwwlknon2  30105  isfrgr  30261  frgrwopreglem3  30315  frgrwopreglem5lem  30321  frgrwopreglem5  30322  isablo  30547  iscbn  30865  hcau  31185  issh  31209  isch  31223  elcnop  31858  ellnop  31859  elbdop  31861  elhmop  31874  elcnfn  31883  ellnfn  31884  isst  32214  ishst  32215  ela  32340  isslmd  33212  elrgspnlem1  33252  elrgspnlem2  33253  elrgspnlem4  33255  elrgspn  33256  ssdifidllem  33465  ssdifidlprm  33467  ssmxidllem  33482  isufd  33549  iscref  33929  isrrext  34085  ispisys  34237  isldsys  34241  isros  34253  issros  34260  oddpwdc  34439  eulerpartleme  34448  eulerpartlemo  34450  eulerpartlemd  34451  eulerpartlemt0  34454  eulerpartlemf  34455  eulerpartlemt  34456  eulerpartlemr  34459  eulerpartlemmf  34460  eulerpartlemgvv  34461  eulerpartlemgs2  34465  eulerpartlemn  34466  elprob  34494  ballotlemelo  34573  ballotleme  34582  bnj1152  35082  bnj1280  35104  subfacp1lem3  35298  subfacp1lem5  35300  erdszelem1  35307  ispconn  35339  issconn  35342  cvmsiota  35393  cvmlift2lem12  35430  fmla1  35503  gonan0  35508  goaln0  35509  gonar  35511  goalr  35513  sategoelfvb  35535  rdgprc0  35907  elwlim  35937  neibastop1  36475  neibastop2lem  36476  neibastop2  36477  topdifinffinlem  37464  pibp19  37531  pibp21  37532  poimirlem5  37738  poimirlem6  37739  poimirlem7  37740  poimirlem8  37741  poimirlem10  37743  poimirlem11  37744  poimirlem12  37745  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem18  37751  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  isprrngo  38163  rabeqel  38364  toycom  39145  isopos  39352  isoml  39410  isatl  39471  iscvlat  39495  ishlat1  39524  cdlemm10N  41290  dihglblem2N  41466  lcfl1lem  41663  lcfls1lem  41706  mapdordlem1a  41806  mapdordlem1  41808  iscsrg  42136  readvcot  42534  mhphflem  42754  pellqrex  43036  islnm  43234  pwssplit4  43246  islnr  43268  fnlimcnv  45827  stoweidlem14  46174  stoweidlem16  46176  stoweidlem37  46197  stoweidlem48  46208  stoweidlem51  46211  stoweidlem59  46219  salexct  46494  salexct2  46499  salexct3  46502  salgencntex  46503  salgensscntex  46504  ovn0lem  46725  opnvonmbllem1  46792  ovolval5lem2  46813  pimincfltioc  46876  pimdecfgtioo  46877  pimincfltioo  46878  smfresal  46948  smfmullem2  46952  smfpimbor1lem1  46958  smfpimbor1lem2  46959  smfinflem  46977  sprsymrelfo  47659  prproropf1olem1  47665  pairreueq  47672  iseven  47790  isodd  47791  m1expevenALTV  47809  iseven2  47813  isodd3  47814  odd2np1ALTV  47836  opoeALTV  47845  opeoALTV  47846  isgbe  47913  isgbow  47914  isgbo  47915  uspgrlimlem2  48151  uspgrlimlem3  48152  uspgrlimlem4  48153  clnbgrvtxedg  48156  grlimpredg  48160  grlimprclnbgrvtx  48161  grlimgrtrilem1  48163  0nodd  48332  1odd  48333  2nodd  48334  iscmgmALT  48386  issgrpALT  48387  iscsgrpALT  48388  1neven  48400  2zlidl  48402  2zrngamgm  48407  2zrngagrp  48411  2zrngmmgm  48414  2zrngnmrid  48418  itsclc0  48933  itsclc0b  48934  isthinc  49580  istermc  49635