Theorem elrab2 3648

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  rru  3736  elrabsf  3783  fvmpti  6995  fvmptss2  7023  tfis  7868  elom  7882  oawordeulem  8567  oeeulem  8615  mapfienlem1  9402  mapfienlem3  9404  mapfien  9405  ordtypelem2  9518  ordtypelem3  9519  ordtypelem9  9525  wemapso2lem  9551  inf3lema  9630  oemapvali  9690  tz9.12lem3  9801  cofsmo  10352  enfin2i  10404  fin23lem28  10423  isf32lem6  10441  hsmexlem4  10512  zorn2lem2  10580  pwfseqlem1  10748  pwfseqlem3  10750  nqereu  11019  elz  12700  zsupss  13069  rpnnen1lem5  13114  elrp  13127  repos  13582  wwlktovf  15116  wwlktovf1  15117  wwlktovfo  15118  01sqrexlem1  15416  01sqrexlem2  15417  01sqrexlem6  15421  01sqrexlem7  15422  ello1  15689  elo1  15700  rlimrege0  15753  divalglem2  16572  divalglem4  16573  divalglem5  16574  divalglem9  16578  divalglem10  16579  bitsfzolem  16611  gcdcllem1  16676  gcdcllem2  16677  gcdcllem3  16678  bezoutlem1  16719  bezoutlem3  16721  bezoutlem4  16722  isprm  16855  maxprmfct  16892  phimullem  16963  eulerthlem1  16965  eulerthlem2  16966  hashgcdlem  16972  pclem  17023  pcprecl  17024  pcprendvds  17025  infpn2  17098  prmreclem1  17101  prmreclem2  17102  prmreclem3  17103  prmreclem5  17105  1arith  17112  elgz  17116  4sqlem13  17142  4sqlem17  17146  4sqlem18  17147  vdwnnlem2  17181  vdwnnlem3  17182  ramtlecl  17185  isdrs  18482  istos  18597  islat  18614  isclat  18681  isdlat  18703  istsr  18764  ischn  18788  issgrp  18916  ismnddef  18932  gsumvallem2  19037  isgrp  19157  elnmz  19380  gastacl  19530  gastacos  19531  symgfixelq  19654  psgneldm  19724  sylow1lem2  19820  sylow1lem4  19822  sylow2alem1  19838  sylow2alem2  19839  efgsdm  19951  iscmn  20010  iscyg  20100  iscyggen  20101  dprdw  20233  ablfacrplem  20288  ablfacrp  20289  ablfac1c  20294  ablfac1eu  20296  pgpfaclem1  20304  ablfaclem3  20310  ablfac2  20312  issimpg  20315  isomnd  20344  isrng  20383  issrg  20421  isring  20470  iscrng  20473  isnzr  20771  islring  20799  isrrg  20957  isdomn  20964  isdrng  20991  isorng  21125  islmod  21146  islvec  21386  lspsolvlem  21427  lbsextlem1  21443  lbsextlem3  21445  lbsextlem4  21446  ssdifidllem  21647  ssdifidlprm  21649  islpir  21659  isphl  21941  pjdm  22020  ishil  22031  frlmssuvc1  22107  frlmssuvc2  22108  frlmsslsp  22109  isassa  22171  psrbag  22232  psrbaglefi  22241  psrbagconcl  22242  psrbagleadd1  22243  gsumbagdiaglem  22246  mplelbas  22305  gsummatr01lem1  22977  gsummatr01lem4  22980  gsummatr01  22981  mretopd  23417  neipeltop  23454  isperf  23476  ist0  23645  ist1  23646  ishaus  23647  iscnrm  23648  isreg  23657  isnrm  23660  ispnrm  23664  iscmp  23713  hauscmplem  23731  isconn  23738  conncompss  23758  is1stc  23766  islly  23794  isnlly  23795  dfac14lem  23943  ishmeo  24085  ptcmplem3  24380  ptcmplem4  24381  istmd  24400  istgp  24403  tgpconncompeqg  24438  tgpt0  24445  qustgpopn  24446  istrg  24490  istdrg  24492  istlm  24511  istvc  24518  iscusp  24624  imasdsf1olem  24699  isxms  24773  isms  24775  blcld  24831  prdsxmslem2  24855  isngp  24922  isnrg  24986  isnlm  25001  icccmplem1  25149  icccmplem2  25150  isclm  25392  iscph  25498  isbn  25666  iscms  25673  ivthlem1  25779  ivthlem2  25780  ivthlem3  25781  elovolm  25803  ovolicc2lem2  25846  ovolicc2lem4  25848  ovolicc2lem5  25849  ismbl  25854  dyadmbllem  25927  dyadmbl  25928  ismbf1  25952  isi1f  26002  isibl  26093  isuc1p  26466  ismon1p  26468  radcnvle  26754  abelthlem2  26766  abelthlem7a  26771  atans  27265  lgamgulmlem2  27364  lgamgulmlem3  27365  lgamgulmlem5  27367  lgambdd  27371  wilthlem2  27403  wilthlem3  27404  ftalem3  27409  sqff1o  27516  mpodvdsmulf1o  27528  dvdsmulf1o  27530  lgslem2  27632  lgslem3  27633  lgsfcl2  27637  rpvmasumlem  27821  dchrvmaeq0  27838  dchrisum0re  27847  pntlem3  27943  elleft  28244  elright  28245  elons  28646  elreno  28884  axcontlem2  29550  lfgredgge2  29709  uspgredg2vlem  29811  uspgredg2v  29812  usgredg2vlem1  29813  usgredg2vlem2  29814  ushgredgedg  29817  ushgredgedgloop  29819  uhgrspan1  29891  upgrreslem  29892  umgrreslem  29893  isfusgr  29906  nbupgrres  29952  nbusgredgeu0  29956  nbusgrf1o0  29957  uvtxel  29976  uvtxel1  29984  cusgrexilem2  30030  cusgrfilem2  30044  vtxdginducedm1lem4  30130  rgrx0ndm  30181  iswspthn  30445  wwlknon  30453  wspthnon  30454  wwlksn0  30459  wwlksnextfun  30494  wwlksnextinj  30495  wwlksnextsurj  30496  wwlksnextproplem3  30507  clwlkclwwlkflem  30602  clwlkclwwlkfolem  30605  isclwwlkn  30625  clwwlkel  30644  clwwlkf  30645  clwwlkf1  30647  isclwwlknon  30689  s2elclwwlknon2  30702  isfrgr  30868  frgrwopreglem3  30922  frgrwopreglem5lem  30928  frgrwopreglem5  30929  isablo  31155  iscbn  31473  hcau  31793  issh  31817  isch  31831  elcnop  32466  ellnop  32467  elbdop  32469  elhmop  32482  elcnfn  32491  ellnfn  32492  isst  32822  ishst  32823  ela  32948  isslmd  33811  elrgspnlem1  33851  elrgspnlem2  33852  elrgspnlem4  33854  elrgspn  33855  ssmxidllem  34046  isufd  34120  iscref  34524  isrrext  34680  ispisys  34833  isldsys  34837  isros  34849  issros  34856  oddpwdc  35034  eulerpartleme  35043  eulerpartlemo  35045  eulerpartlemd  35046  eulerpartlemt0  35049  eulerpartlemf  35050  eulerpartlemt  35051  eulerpartlemr  35054  eulerpartlemmf  35055  eulerpartlemgvv  35056  eulerpartlemgs2  35060  eulerpartlemn  35061  elprob  35089  ballotlemelo  35168  ballotleme  35177  bnj1152  35676  bnj1280  35698  elscott  35797  elscott2  35800  elscottrank  35801  subfacp1lem3  36035  subfacp1lem5  36037  erdszelem1  36044  ispconn  36076  issconn  36079  cvmsiota  36130  cvmlift2lem12  36167  fmla1  36240  gonan0  36245  goaln0  36246  gonar  36248  goalr  36250  sategoelfvb  36272  mirimanoffr  36548  cardprcr  36552  rdgprc0  36649  elwlim  36679  neibastop1  37241  neibastop2lem  37242  neibastop2  37243  topdifinffinlem  38377  pibp19  38444  pibp21  38445  poimirlem5  38650  poimirlem6  38651  poimirlem7  38652  poimirlem8  38653  poimirlem10  38655  poimirlem11  38656  poimirlem12  38657  poimirlem15  38660  poimirlem16  38661  poimirlem17  38662  poimirlem18  38663  poimirlem19  38664  poimirlem20  38665  poimirlem21  38666  poimirlem22  38667  isprrngo  39091  rabeqel  39296  toycom  40137  isopos  40344  isoml  40402  isatl  40463  iscvlat  40487  ishlat1  40516  cdlemm10N  42282  dihglblem2N  42458  lcfl1lem  42655  lcfls1lem  42698  mapdordlem1a  42798  mapdordlem1  42800  iscsrg  43128  readvcot  43522  mhphflem  43731  pellqrex  43993  islnm  44186  pwssplit4  44198  islnr  44220  fnlimcnv  46784  stoweidlem14  47131  stoweidlem16  47133  stoweidlem37  47154  stoweidlem48  47165  stoweidlem51  47168  stoweidlem59  47176  salexct  47451  salexct2  47456  salexct3  47459  salgencntex  47460  salgensscntex  47461  ovn0lem  47682  opnvonmbllem1  47749  ovolval5lem2  47770  pimincfltioc  47833  pimdecfgtioo  47834  pimincfltioo  47835  smfresal  47905  smfmullem2  47909  smfpimbor1lem1  47915  smfpimbor1lem2  47916  smfinflem  47934  sprsymrelfo  48686  prproropf1olem1  48692  pairreueq  48699  iseven  48833  isodd  48834  m1expevenALTV  48852  iseven2  48856  isodd3  48857  odd2np1ALTV  48879  opoeALTV  48888  opeoALTV  48889  isgbe  48956  isgbow  48957  isgbo  48958  uspgrlimlem2  49194  uspgrlimlem3  49195  uspgrlimlem4  49196  clnbgrvtxedg  49199  grlimpredg  49203  grlimprclnbgrvtx  49204  grlimgrtrilem1  49206  0nodd  49374  1odd  49375  2nodd  49376  iscmgmALT  49428  issgrpALT  49429  iscsgrpALT  49430  1neven  49442  2zlidl  49444  2zrngamgm  49449  2zrngagrp  49453  2zrngmmgm  49456  2zrngnmrid  49460  isprmrng  49540  itsclc0  49990  itsclc0b  49991  isthinc  50661  istermc  50716