Theorem elrab2 3605

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  {crab 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410

This theorem is referenced by:  rru  3692  elrabsf  3742  fvmpti  6817  fvmptss2  6843  tfis  7633  elom  7647  oawordeulem  8282  oeeulem  8329  mapfienlem1  9021  mapfienlem3  9023  mapfien  9024  ordtypelem2  9135  ordtypelem3  9136  ordtypelem9  9142  wemapso2lem  9168  inf3lema  9239  oemapvali  9299  tz9.12lem3  9405  cofsmo  9883  enfin2i  9935  fin23lem28  9954  isf32lem6  9972  hsmexlem4  10043  zorn2lem2  10111  pwfseqlem1  10272  pwfseqlem3  10274  nqereu  10543  elz  12178  zsupss  12533  rpnnen1lem5  12577  elrp  12588  repos  13034  wwlktovf  14523  wwlktovf1  14524  wwlktovfo  14525  sqrlem1  14806  sqrlem2  14807  sqrlem6  14811  sqrlem7  14812  ello1  15076  elo1  15087  rlimrege0  15140  divalglem2  15956  divalglem4  15957  divalglem5  15958  divalglem9  15962  divalglem10  15963  bitsfzolem  15993  gcdcllem1  16058  gcdcllem2  16059  gcdcllem3  16060  bezoutlem1  16099  bezoutlem3  16101  bezoutlem4  16102  isprm  16230  maxprmfct  16266  phimullem  16332  eulerthlem1  16334  eulerthlem2  16335  hashgcdlem  16341  pclem  16391  pcprecl  16392  pcprendvds  16393  infpn2  16466  prmreclem1  16469  prmreclem2  16470  prmreclem3  16471  prmreclem5  16473  1arith  16480  elgz  16484  4sqlem13  16510  4sqlem17  16514  4sqlem18  16515  vdwnnlem2  16549  vdwnnlem3  16550  ramtlecl  16553  isdrs  17808  istos  17924  islat  17939  isclat  18006  isdlat  18028  istsr  18089  issgrp  18164  ismnddef  18175  gsumvallem2  18260  isgrp  18371  elnmz  18579  gastacl  18703  gastacos  18704  symgfixelq  18825  psgneldm  18895  sylow1lem2  18988  sylow1lem4  18990  sylow2alem1  19006  sylow2alem2  19007  efgsdm  19120  iscmn  19178  iscyg  19263  iscyggen  19264  dprdw  19397  ablfacrplem  19452  ablfacrp  19453  ablfac1c  19458  ablfac1eu  19460  pgpfaclem1  19468  ablfaclem3  19474  ablfac2  19476  issimpg  19479  issrg  19522  isring  19566  iscrng  19569  isdrng  19771  islmod  19903  islvec  20141  lspsolvlem  20179  lbsextlem1  20195  lbsextlem3  20197  lbsextlem4  20198  islpir  20287  isnzr  20297  isrrg  20326  isdomn  20332  isphl  20590  pjdm  20669  ishil  20680  frlmssuvc1  20756  frlmssuvc2  20757  frlmsslsp  20758  isassa  20818  psrbag  20876  psrbaglefi  20891  psrbaglefiOLD  20892  psrbagconcl  20893  psrbagconclOLD  20894  psrbagconf1oOLD  20896  gsumbagdiaglemOLD  20897  gsumbagdiaglem  20900  mplelbas  20955  gsummatr01lem1  21552  gsummatr01lem4  21555  gsummatr01  21556  mretopd  21989  neipeltop  22026  isperf  22048  ist0  22217  ist1  22218  ishaus  22219  iscnrm  22220  isreg  22229  isnrm  22232  ispnrm  22236  iscmp  22285  hauscmplem  22303  isconn  22310  conncompss  22330  is1stc  22338  islly  22365  isnlly  22366  dfac14lem  22514  ishmeo  22656  ptcmplem3  22951  ptcmplem4  22952  istmd  22971  istgp  22974  tgpconncompeqg  23009  tgpt0  23016  qustgpopn  23017  istrg  23061  istdrg  23063  istlm  23082  istvc  23089  iscusp  23196  imasdsf1olem  23271  isxms  23345  isms  23347  blcld  23403  prdsxmslem2  23427  isngp  23494  isnrg  23558  isnlm  23573  icccmplem1  23719  icccmplem2  23720  isclm  23961  iscph  24067  isbn  24235  iscms  24242  ivthlem1  24348  ivthlem2  24349  ivthlem3  24350  elovolm  24372  ovolicc2lem2  24415  ovolicc2lem4  24417  ovolicc2lem5  24418  ismbl  24423  dyadmbllem  24496  dyadmbl  24497  ismbf1  24521  isi1f  24571  isibl  24663  isuc1p  25038  ismon1p  25040  radcnvle  25312  abelthlem2  25324  abelthlem7a  25329  atans  25813  lgamgulmlem2  25912  lgamgulmlem3  25913  lgamgulmlem5  25915  lgambdd  25919  wilthlem2  25951  wilthlem3  25952  ftalem3  25957  sqff1o  26064  dvdsmulf1o  26076  lgslem2  26179  lgslem3  26180  lgsfcl2  26184  rpvmasumlem  26368  dchrvmaeq0  26385  dchrisum0re  26394  pntlem3  26490  axcontlem2  27056  lfgredgge2  27215  uspgredg2vlem  27311  uspgredg2v  27312  usgredg2vlem1  27313  usgredg2vlem2  27314  ushgredgedg  27317  ushgredgedgloop  27319  uhgrspan1  27391  upgrreslem  27392  umgrreslem  27393  isfusgr  27406  nbupgrres  27452  nbusgredgeu0  27456  nbusgrf1o0  27457  uvtxel  27476  uvtxel1  27484  cusgrexilem2  27530  cusgrfilem2  27544  vtxdginducedm1lem4  27630  rgrx0ndm  27681  iswspthn  27933  wwlknon  27941  wspthnon  27942  wwlksn0  27947  wwlksnextfun  27982  wwlksnextinj  27983  wwlksnextsurj  27984  wwlksnextproplem3  27995  clwlkclwwlkflem  28087  clwlkclwwlkfolem  28090  isclwwlkn  28110  clwwlkel  28129  clwwlkf  28130  clwwlkf1  28132  isclwwlknon  28174  s2elclwwlknon2  28187  isfrgr  28343  frgrwopreglem3  28397  frgrwopreglem5lem  28403  frgrwopreglem5  28404  isablo  28627  iscbn  28945  hcau  29265  issh  29289  isch  29303  elcnop  29938  ellnop  29939  elbdop  29941  elhmop  29954  elcnfn  29963  ellnfn  29964  isst  30294  ishst  30295  ela  30420  isomnd  31046  isslmd  31174  isorng  31217  ssmxidllem  31355  isufd  31377  iscref  31508  isrrext  31662  ispisys  31832  isldsys  31836  isros  31848  issros  31855  oddpwdc  32033  eulerpartleme  32042  eulerpartlemo  32044  eulerpartlemd  32045  eulerpartlemt0  32048  eulerpartlemf  32049  eulerpartlemt  32050  eulerpartlemr  32053  eulerpartlemmf  32054  eulerpartlemgvv  32055  eulerpartlemgs2  32059  eulerpartlemn  32060  elprob  32088  ballotlemelo  32166  ballotleme  32175  bnj1152  32691  bnj1280  32713  subfacp1lem3  32857  subfacp1lem5  32859  erdszelem1  32866  ispconn  32898  issconn  32901  cvmsiota  32952  cvmlift2lem12  32989  fmla1  33062  gonan0  33067  goaln0  33068  gonar  33070  goalr  33072  sategoelfvb  33094  rdgprc0  33488  elwlim  33554  neibastop1  34285  neibastop2lem  34286  neibastop2  34287  topdifinffinlem  35255  pibp19  35322  pibp21  35323  poimirlem5  35519  poimirlem6  35520  poimirlem7  35521  poimirlem8  35522  poimirlem10  35524  poimirlem11  35525  poimirlem12  35526  poimirlem15  35529  poimirlem16  35530  poimirlem17  35531  poimirlem18  35532  poimirlem19  35533  poimirlem20  35534  poimirlem21  35535  poimirlem22  35536  isprrngo  35945  rabeqel  36131  toycom  36724  isopos  36931  isoml  36989  isatl  37050  iscvlat  37074  ishlat1  37103  cdlemm10N  38869  dihglblem2N  39045  lcfl1lem  39242  lcfls1lem  39285  mapdordlem1a  39385  mapdordlem1  39387  mhphflem  39994  pellqrex  40404  islnm  40605  pwssplit4  40617  islnr  40639  fnlimcnv  42883  stoweidlem14  43230  stoweidlem16  43232  stoweidlem37  43253  stoweidlem48  43264  stoweidlem51  43267  stoweidlem59  43275  salexct  43548  salexct2  43553  salexct3  43556  salgencntex  43557  salgensscntex  43558  ovn0lem  43778  opnvonmbllem1  43845  ovolval5lem2  43866  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  smfresal  43994  smfmullem2  43998  smfpimbor1lem1  44004  smfpimbor1lem2  44005  smfinflem  44022  sprsymrelfo  44622  prproropf1olem1  44628  pairreueq  44635  iseven  44753  isodd  44754  m1expevenALTV  44772  iseven2  44776  isodd3  44777  odd2np1ALTV  44799  opoeALTV  44808  opeoALTV  44809  isgbe  44876  isgbow  44877  isgbo  44878  0nodd  45037  1odd  45038  2nodd  45039  iscmgmALT  45091  issgrpALT  45092  iscsgrpALT  45093  isrng  45107  1neven  45163  2zlidl  45165  2zrngamgm  45170  2zrngagrp  45174  2zrngmmgm  45177  2zrngnmrid  45181  itsclc0  45790  itsclc0b  45791  isthinc  45975