Theorem elrab2 3645

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 2823	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3642	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 275	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438

This theorem is referenced by:  rru  3733  elrabsf  3782  fvmpti  6923  fvmptss2  6950  tfis  7780  elom  7794  oawordeulem  8464  oeeulem  8511  mapfienlem1  9284  mapfienlem3  9286  mapfien  9287  ordtypelem2  9400  ordtypelem3  9401  ordtypelem9  9407  wemapso2lem  9433  inf3lema  9509  oemapvali  9569  tz9.12lem3  9677  cofsmo  10155  enfin2i  10207  fin23lem28  10226  isf32lem6  10244  hsmexlem4  10315  zorn2lem2  10383  pwfseqlem1  10544  pwfseqlem3  10546  nqereu  10815  elz  12465  zsupss  12830  rpnnen1lem5  12874  elrp  12887  repos  13341  wwlktovf  14858  wwlktovf1  14859  wwlktovfo  14860  01sqrexlem1  15144  01sqrexlem2  15145  01sqrexlem6  15149  01sqrexlem7  15150  ello1  15417  elo1  15428  rlimrege0  15481  divalglem2  16301  divalglem4  16302  divalglem5  16303  divalglem9  16307  divalglem10  16308  bitsfzolem  16340  gcdcllem1  16405  gcdcllem2  16406  gcdcllem3  16407  bezoutlem1  16445  bezoutlem3  16447  bezoutlem4  16448  isprm  16579  maxprmfct  16615  phimullem  16685  eulerthlem1  16687  eulerthlem2  16688  hashgcdlem  16694  pclem  16745  pcprecl  16746  pcprendvds  16747  infpn2  16820  prmreclem1  16823  prmreclem2  16824  prmreclem3  16825  prmreclem5  16827  1arith  16834  elgz  16838  4sqlem13  16864  4sqlem17  16868  4sqlem18  16869  vdwnnlem2  16903  vdwnnlem3  16904  ramtlecl  16907  isdrs  18202  istos  18317  islat  18334  isclat  18401  isdlat  18423  istsr  18484  ischn  18508  issgrp  18623  ismnddef  18639  gsumvallem2  18737  isgrp  18847  elnmz  19070  gastacl  19216  gastacos  19217  symgfixelq  19340  psgneldm  19410  sylow1lem2  19506  sylow1lem4  19508  sylow2alem1  19524  sylow2alem2  19525  efgsdm  19637  iscmn  19696  iscyg  19786  iscyggen  19787  dprdw  19919  ablfacrplem  19974  ablfacrp  19975  ablfac1c  19980  ablfac1eu  19982  pgpfaclem1  19990  ablfaclem3  19996  ablfac2  19998  issimpg  20001  isomnd  20030  isrng  20067  issrg  20101  isring  20150  iscrng  20153  isnzr  20424  islring  20450  isrrg  20608  isdomn  20615  isdrng  20643  isorng  20771  islmod  20792  islvec  21033  lspsolvlem  21074  lbsextlem1  21090  lbsextlem3  21092  lbsextlem4  21093  islpir  21260  isphl  21560  pjdm  21639  ishil  21650  frlmssuvc1  21726  frlmssuvc2  21727  frlmsslsp  21728  isassa  21788  psrbag  21849  psrbaglefi  21858  psrbagconcl  21859  psrbagleadd1  21860  gsumbagdiaglem  21862  mplelbas  21923  gsummatr01lem1  22565  gsummatr01lem4  22568  gsummatr01  22569  mretopd  23002  neipeltop  23039  isperf  23061  ist0  23230  ist1  23231  ishaus  23232  iscnrm  23233  isreg  23242  isnrm  23245  ispnrm  23249  iscmp  23298  hauscmplem  23316  isconn  23323  conncompss  23343  is1stc  23351  islly  23378  isnlly  23379  dfac14lem  23527  ishmeo  23669  ptcmplem3  23964  ptcmplem4  23965  istmd  23984  istgp  23987  tgpconncompeqg  24022  tgpt0  24029  qustgpopn  24030  istrg  24074  istdrg  24076  istlm  24095  istvc  24102  iscusp  24208  imasdsf1olem  24283  isxms  24357  isms  24359  blcld  24415  prdsxmslem2  24439  isngp  24506  isnrg  24570  isnlm  24585  icccmplem1  24733  icccmplem2  24734  isclm  24986  iscph  25092  isbn  25260  iscms  25267  ivthlem1  25374  ivthlem2  25375  ivthlem3  25376  elovolm  25398  ovolicc2lem2  25441  ovolicc2lem4  25443  ovolicc2lem5  25444  ismbl  25449  dyadmbllem  25522  dyadmbl  25523  ismbf1  25547  isi1f  25597  isibl  25688  isuc1p  26068  ismon1p  26070  radcnvle  26351  abelthlem2  26364  abelthlem7a  26369  atans  26862  lgamgulmlem2  26962  lgamgulmlem3  26963  lgamgulmlem5  26965  lgambdd  26969  wilthlem2  27001  wilthlem3  27002  ftalem3  27007  sqff1o  27114  mpodvdsmulf1o  27126  dvdsmulf1o  27128  lgslem2  27231  lgslem3  27232  lgsfcl2  27236  rpvmasumlem  27420  dchrvmaeq0  27437  dchrisum0re  27446  pntlem3  27542  elleft  27801  elright  27802  elons  28185  elreno  28392  axcontlem2  28938  lfgredgge2  29097  uspgredg2vlem  29196  uspgredg2v  29197  usgredg2vlem1  29198  usgredg2vlem2  29199  ushgredgedg  29202  ushgredgedgloop  29204  uhgrspan1  29276  upgrreslem  29277  umgrreslem  29278  isfusgr  29291  nbupgrres  29337  nbusgredgeu0  29341  nbusgrf1o0  29342  uvtxel  29361  uvtxel1  29369  cusgrexilem2  29415  cusgrfilem2  29430  vtxdginducedm1lem4  29516  rgrx0ndm  29567  iswspthn  29822  wwlknon  29830  wspthnon  29831  wwlksn0  29836  wwlksnextfun  29871  wwlksnextinj  29872  wwlksnextsurj  29873  wwlksnextproplem3  29884  clwlkclwwlkflem  29976  clwlkclwwlkfolem  29979  isclwwlkn  29999  clwwlkel  30018  clwwlkf  30019  clwwlkf1  30021  isclwwlknon  30063  s2elclwwlknon2  30076  isfrgr  30232  frgrwopreglem3  30286  frgrwopreglem5lem  30292  frgrwopreglem5  30293  isablo  30518  iscbn  30836  hcau  31156  issh  31180  isch  31194  elcnop  31829  ellnop  31830  elbdop  31832  elhmop  31845  elcnfn  31854  ellnfn  31855  isst  32185  ishst  32186  ela  32311  isslmd  33163  elrgspnlem1  33201  elrgspnlem2  33202  elrgspnlem4  33204  elrgspn  33205  ssdifidllem  33413  ssdifidlprm  33415  ssmxidllem  33430  isufd  33497  iscref  33849  isrrext  34005  ispisys  34157  isldsys  34161  isros  34173  issros  34180  oddpwdc  34359  eulerpartleme  34368  eulerpartlemo  34370  eulerpartlemd  34371  eulerpartlemt0  34374  eulerpartlemf  34375  eulerpartlemt  34376  eulerpartlemr  34379  eulerpartlemmf  34380  eulerpartlemgvv  34381  eulerpartlemgs2  34385  eulerpartlemn  34386  elprob  34414  ballotlemelo  34493  ballotleme  34502  bnj1152  35002  bnj1280  35024  subfacp1lem3  35218  subfacp1lem5  35220  erdszelem1  35227  ispconn  35259  issconn  35262  cvmsiota  35313  cvmlift2lem12  35350  fmla1  35423  gonan0  35428  goaln0  35429  gonar  35431  goalr  35433  sategoelfvb  35455  rdgprc0  35827  elwlim  35857  neibastop1  36393  neibastop2lem  36394  neibastop2  36395  topdifinffinlem  37381  pibp19  37448  pibp21  37449  poimirlem5  37665  poimirlem6  37666  poimirlem7  37667  poimirlem8  37668  poimirlem10  37670  poimirlem11  37671  poimirlem12  37672  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem18  37678  poimirlem19  37679  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  isprrngo  38090  rabeqel  38289  toycom  39012  isopos  39219  isoml  39277  isatl  39338  iscvlat  39362  ishlat1  39391  cdlemm10N  41157  dihglblem2N  41333  lcfl1lem  41530  lcfls1lem  41573  mapdordlem1a  41673  mapdordlem1  41675  iscsrg  42003  readvcot  42397  mhphflem  42629  pellqrex  42912  islnm  43110  pwssplit4  43122  islnr  43144  fnlimcnv  45705  stoweidlem14  46052  stoweidlem16  46054  stoweidlem37  46075  stoweidlem48  46086  stoweidlem51  46089  stoweidlem59  46097  salexct  46372  salexct2  46377  salexct3  46380  salgencntex  46381  salgensscntex  46382  ovn0lem  46603  opnvonmbllem1  46670  ovolval5lem2  46691  pimincfltioc  46754  pimdecfgtioo  46755  pimincfltioo  46756  smfresal  46826  smfmullem2  46830  smfpimbor1lem1  46836  smfpimbor1lem2  46837  smfinflem  46855  sprsymrelfo  47528  prproropf1olem1  47534  pairreueq  47541  iseven  47659  isodd  47660  m1expevenALTV  47678  iseven2  47682  isodd3  47683  odd2np1ALTV  47705  opoeALTV  47714  opeoALTV  47715  isgbe  47782  isgbow  47783  isgbo  47784  uspgrlimlem2  48020  uspgrlimlem3  48021  uspgrlimlem4  48022  clnbgrvtxedg  48025  grlimpredg  48029  grlimprclnbgrvtx  48030  grlimgrtrilem1  48032  0nodd  48201  1odd  48202  2nodd  48203  iscmgmALT  48255  issgrpALT  48256  iscsgrpALT  48257  1neven  48269  2zlidl  48271  2zrngamgm  48276  2zrngagrp  48280  2zrngmmgm  48283  2zrngnmrid  48287  itsclc0  48803  itsclc0b  48804  isthinc  49451  istermc  49506