Theorem elrab2 3647

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435

This theorem is referenced by:  rru  3735  elrabsf  3784  fvmpti  6922  fvmptss2  6949  tfis  7779  elom  7793  oawordeulem  8463  oeeulem  8510  mapfienlem1  9283  mapfienlem3  9285  mapfien  9286  ordtypelem2  9399  ordtypelem3  9400  ordtypelem9  9406  wemapso2lem  9432  inf3lema  9508  oemapvali  9568  tz9.12lem3  9673  cofsmo  10151  enfin2i  10203  fin23lem28  10222  isf32lem6  10240  hsmexlem4  10311  zorn2lem2  10379  pwfseqlem1  10540  pwfseqlem3  10542  nqereu  10811  elz  12461  zsupss  12826  rpnnen1lem5  12870  elrp  12883  repos  13337  wwlktovf  14850  wwlktovf1  14851  wwlktovfo  14852  01sqrexlem1  15136  01sqrexlem2  15137  01sqrexlem6  15141  01sqrexlem7  15142  ello1  15409  elo1  15420  rlimrege0  15473  divalglem2  16293  divalglem4  16294  divalglem5  16295  divalglem9  16299  divalglem10  16300  bitsfzolem  16332  gcdcllem1  16397  gcdcllem2  16398  gcdcllem3  16399  bezoutlem1  16437  bezoutlem3  16439  bezoutlem4  16440  isprm  16571  maxprmfct  16607  phimullem  16677  eulerthlem1  16679  eulerthlem2  16680  hashgcdlem  16686  pclem  16737  pcprecl  16738  pcprendvds  16739  infpn2  16812  prmreclem1  16815  prmreclem2  16816  prmreclem3  16817  prmreclem5  16819  1arith  16826  elgz  16830  4sqlem13  16856  4sqlem17  16860  4sqlem18  16861  vdwnnlem2  16895  vdwnnlem3  16896  ramtlecl  16899  isdrs  18194  istos  18309  islat  18326  isclat  18393  isdlat  18415  istsr  18476  issgrp  18581  ismnddef  18597  gsumvallem2  18695  isgrp  18805  elnmz  19029  gastacl  19175  gastacos  19176  symgfixelq  19299  psgneldm  19369  sylow1lem2  19465  sylow1lem4  19467  sylow2alem1  19483  sylow2alem2  19484  efgsdm  19596  iscmn  19655  iscyg  19745  iscyggen  19746  dprdw  19878  ablfacrplem  19933  ablfacrp  19934  ablfac1c  19939  ablfac1eu  19941  pgpfaclem1  19949  ablfaclem3  19955  ablfac2  19957  issimpg  19960  isomnd  19989  isrng  20026  issrg  20060  isring  20109  iscrng  20112  isnzr  20383  islring  20409  isrrg  20567  isdomn  20574  isdrng  20602  isorng  20730  islmod  20751  islvec  20992  lspsolvlem  21033  lbsextlem1  21049  lbsextlem3  21051  lbsextlem4  21052  islpir  21219  isphl  21519  pjdm  21598  ishil  21609  frlmssuvc1  21685  frlmssuvc2  21686  frlmsslsp  21687  isassa  21747  psrbag  21808  psrbaglefi  21817  psrbagconcl  21818  psrbagleadd1  21819  gsumbagdiaglem  21821  mplelbas  21882  gsummatr01lem1  22524  gsummatr01lem4  22527  gsummatr01  22528  mretopd  22961  neipeltop  22998  isperf  23020  ist0  23189  ist1  23190  ishaus  23191  iscnrm  23192  isreg  23201  isnrm  23204  ispnrm  23208  iscmp  23257  hauscmplem  23275  isconn  23282  conncompss  23302  is1stc  23310  islly  23337  isnlly  23338  dfac14lem  23486  ishmeo  23628  ptcmplem3  23923  ptcmplem4  23924  istmd  23943  istgp  23946  tgpconncompeqg  23981  tgpt0  23988  qustgpopn  23989  istrg  24033  istdrg  24035  istlm  24054  istvc  24061  iscusp  24167  imasdsf1olem  24242  isxms  24316  isms  24318  blcld  24374  prdsxmslem2  24398  isngp  24465  isnrg  24529  isnlm  24544  icccmplem1  24692  icccmplem2  24693  isclm  24945  iscph  25051  isbn  25219  iscms  25226  ivthlem1  25333  ivthlem2  25334  ivthlem3  25335  elovolm  25357  ovolicc2lem2  25400  ovolicc2lem4  25402  ovolicc2lem5  25403  ismbl  25408  dyadmbllem  25481  dyadmbl  25482  ismbf1  25506  isi1f  25556  isibl  25647  isuc1p  26027  ismon1p  26029  radcnvle  26310  abelthlem2  26323  abelthlem7a  26328  atans  26821  lgamgulmlem2  26921  lgamgulmlem3  26922  lgamgulmlem5  26924  lgambdd  26928  wilthlem2  26960  wilthlem3  26961  ftalem3  26966  sqff1o  27073  mpodvdsmulf1o  27085  dvdsmulf1o  27087  lgslem2  27190  lgslem3  27191  lgsfcl2  27195  rpvmasumlem  27379  dchrvmaeq0  27396  dchrisum0re  27405  pntlem3  27501  elleft  27760  elright  27761  elons  28144  elreno  28351  axcontlem2  28897  lfgredgge2  29056  uspgredg2vlem  29155  uspgredg2v  29156  usgredg2vlem1  29157  usgredg2vlem2  29158  ushgredgedg  29161  ushgredgedgloop  29163  uhgrspan1  29235  upgrreslem  29236  umgrreslem  29237  isfusgr  29250  nbupgrres  29296  nbusgredgeu0  29300  nbusgrf1o0  29301  uvtxel  29320  uvtxel1  29328  cusgrexilem2  29374  cusgrfilem2  29389  vtxdginducedm1lem4  29475  rgrx0ndm  29526  iswspthn  29781  wwlknon  29789  wspthnon  29790  wwlksn0  29795  wwlksnextfun  29830  wwlksnextinj  29831  wwlksnextsurj  29832  wwlksnextproplem3  29843  clwlkclwwlkflem  29935  clwlkclwwlkfolem  29938  isclwwlkn  29958  clwwlkel  29977  clwwlkf  29978  clwwlkf1  29980  isclwwlknon  30022  s2elclwwlknon2  30035  isfrgr  30191  frgrwopreglem3  30245  frgrwopreglem5lem  30251  frgrwopreglem5  30252  isablo  30477  iscbn  30795  hcau  31115  issh  31139  isch  31153  elcnop  31788  ellnop  31789  elbdop  31791  elhmop  31804  elcnfn  31813  ellnfn  31814  isst  32144  ishst  32145  ela  32270  ischn  32943  isslmd  33139  elrgspnlem1  33177  elrgspnlem2  33178  elrgspnlem4  33180  elrgspn  33181  ssdifidllem  33389  ssdifidlprm  33391  ssmxidllem  33406  isufd  33473  iscref  33825  isrrext  33981  ispisys  34133  isldsys  34137  isros  34149  issros  34156  oddpwdc  34335  eulerpartleme  34344  eulerpartlemo  34346  eulerpartlemd  34347  eulerpartlemt0  34350  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgs2  34361  eulerpartlemn  34362  elprob  34390  ballotlemelo  34469  ballotleme  34478  bnj1152  34978  bnj1280  35000  subfacp1lem3  35172  subfacp1lem5  35174  erdszelem1  35181  ispconn  35213  issconn  35216  cvmsiota  35267  cvmlift2lem12  35304  fmla1  35377  gonan0  35382  goaln0  35383  gonar  35385  goalr  35387  sategoelfvb  35409  rdgprc0  35784  elwlim  35814  neibastop1  36350  neibastop2lem  36351  neibastop2  36352  topdifinffinlem  37338  pibp19  37405  pibp21  37406  poimirlem5  37622  poimirlem6  37623  poimirlem7  37624  poimirlem8  37625  poimirlem10  37627  poimirlem11  37628  poimirlem12  37629  poimirlem15  37632  poimirlem16  37633  poimirlem17  37634  poimirlem18  37635  poimirlem19  37636  poimirlem20  37637  poimirlem21  37638  poimirlem22  37639  isprrngo  38047  rabeqel  38246  toycom  38969  isopos  39176  isoml  39234  isatl  39295  iscvlat  39319  ishlat1  39348  cdlemm10N  41114  dihglblem2N  41290  lcfl1lem  41487  lcfls1lem  41530  mapdordlem1a  41630  mapdordlem1  41632  iscsrg  41960  readvcot  42354  mhphflem  42586  pellqrex  42869  islnm  43067  pwssplit4  43079  islnr  43101  fnlimcnv  45662  stoweidlem14  46009  stoweidlem16  46011  stoweidlem37  46032  stoweidlem48  46043  stoweidlem51  46046  stoweidlem59  46054  salexct  46329  salexct2  46334  salexct3  46337  salgencntex  46338  salgensscntex  46339  ovn0lem  46560  opnvonmbllem1  46627  ovolval5lem2  46648  pimincfltioc  46711  pimdecfgtioo  46712  pimincfltioo  46713  smfresal  46783  smfmullem2  46787  smfpimbor1lem1  46793  smfpimbor1lem2  46794  smfinflem  46812  sprsymrelfo  47495  prproropf1olem1  47501  pairreueq  47508  iseven  47626  isodd  47627  m1expevenALTV  47645  iseven2  47649  isodd3  47650  odd2np1ALTV  47672  opoeALTV  47681  opeoALTV  47682  isgbe  47749  isgbow  47750  isgbo  47751  uspgrlimlem2  47987  uspgrlimlem3  47988  uspgrlimlem4  47989  clnbgrvtxedg  47992  grlimpredg  47996  grlimprclnbgrvtx  47997  grlimgrtrilem1  47999  0nodd  48168  1odd  48169  2nodd  48170  iscmgmALT  48222  issgrpALT  48223  iscsgrpALT  48224  1neven  48236  2zlidl  48238  2zrngamgm  48243  2zrngagrp  48247  2zrngmmgm  48250  2zrngnmrid  48254  itsclc0  48770  itsclc0b  48771  isthinc  49418  istermc  49473