Theorem elrab2 3649

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 3645	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 278	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  rru  3737  elrabsf  3784  fvmpti  6985  fvmptss2  7013  tfis  7851  elom  7865  oawordeulem  8541  oeeulem  8589  mapfienlem1  9375  mapfienlem3  9377  mapfien  9378  ordtypelem2  9491  ordtypelem3  9492  ordtypelem9  9498  wemapso2lem  9524  inf3lema  9603  oemapvali  9663  tz9.12lem3  9771  cofsmo  10271  enfin2i  10323  fin23lem28  10342  isf32lem6  10360  hsmexlem4  10431  zorn2lem2  10499  pwfseqlem1  10667  pwfseqlem3  10669  nqereu  10938  elz  12617  zsupss  12986  rpnnen1lem5  13031  elrp  13044  repos  13499  wwlktovf  15029  wwlktovf1  15030  wwlktovfo  15031  01sqrexlem1  15329  01sqrexlem2  15330  01sqrexlem6  15334  01sqrexlem7  15335  ello1  15602  elo1  15613  rlimrege0  15666  divalglem2  16485  divalglem4  16486  divalglem5  16487  divalglem9  16491  divalglem10  16492  bitsfzolem  16524  gcdcllem1  16589  gcdcllem2  16590  gcdcllem3  16591  bezoutlem1  16629  bezoutlem3  16631  bezoutlem4  16632  isprm  16763  maxprmfct  16800  phimullem  16870  eulerthlem1  16872  eulerthlem2  16873  hashgcdlem  16879  pclem  16930  pcprecl  16931  pcprendvds  16932  infpn2  17005  prmreclem1  17008  prmreclem2  17009  prmreclem3  17010  prmreclem5  17012  1arith  17019  elgz  17023  4sqlem13  17049  4sqlem17  17053  4sqlem18  17054  vdwnnlem2  17088  vdwnnlem3  17089  ramtlecl  17092  isdrs  18389  istos  18504  islat  18521  isclat  18588  isdlat  18610  istsr  18671  ischn  18695  issgrp  18822  ismnddef  18838  gsumvallem2  18943  isgrp  19063  elnmz  19286  gastacl  19436  gastacos  19437  symgfixelq  19560  psgneldm  19630  sylow1lem2  19726  sylow1lem4  19728  sylow2alem1  19744  sylow2alem2  19745  efgsdm  19857  iscmn  19916  iscyg  20006  iscyggen  20007  dprdw  20139  ablfacrplem  20194  ablfacrp  20195  ablfac1c  20200  ablfac1eu  20202  pgpfaclem1  20210  ablfaclem3  20216  ablfac2  20218  issimpg  20221  isomnd  20250  isrng  20289  issrg  20327  isring  20376  iscrng  20379  isnzr  20674  islring  20702  isrrg  20860  isdomn  20867  isdrng  20894  isorng  21027  islmod  21048  islvec  21288  lspsolvlem  21329  lbsextlem1  21345  lbsextlem3  21347  lbsextlem4  21348  ssdifidllem  21547  ssdifidlprm  21549  islpir  21559  isphl  21841  pjdm  21920  ishil  21931  frlmssuvc1  22007  frlmssuvc2  22008  frlmsslsp  22009  isassa  22071  psrbag  22132  psrbaglefi  22141  psrbagconcl  22142  psrbagleadd1  22143  gsumbagdiaglem  22146  mplelbas  22205  gsummatr01lem1  22877  gsummatr01lem4  22880  gsummatr01  22881  mretopd  23317  neipeltop  23354  isperf  23376  ist0  23545  ist1  23546  ishaus  23547  iscnrm  23548  isreg  23557  isnrm  23560  ispnrm  23564  iscmp  23613  hauscmplem  23631  isconn  23638  conncompss  23658  is1stc  23666  islly  23694  isnlly  23695  dfac14lem  23843  ishmeo  23985  ptcmplem3  24280  ptcmplem4  24281  istmd  24300  istgp  24303  tgpconncompeqg  24338  tgpt0  24345  qustgpopn  24346  istrg  24390  istdrg  24392  istlm  24411  istvc  24418  iscusp  24524  imasdsf1olem  24599  isxms  24673  isms  24675  blcld  24731  prdsxmslem2  24755  isngp  24822  isnrg  24886  isnlm  24901  icccmplem1  25049  icccmplem2  25050  isclm  25292  iscph  25398  isbn  25566  iscms  25573  ivthlem1  25679  ivthlem2  25680  ivthlem3  25681  elovolm  25703  ovolicc2lem2  25746  ovolicc2lem4  25748  ovolicc2lem5  25749  ismbl  25754  dyadmbllem  25827  dyadmbl  25828  ismbf1  25852  isi1f  25902  isibl  25993  isuc1p  26366  ismon1p  26368  radcnvle  26656  abelthlem2  26668  abelthlem7a  26673  atans  27167  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem5  27269  lgambdd  27273  wilthlem2  27305  wilthlem3  27306  ftalem3  27311  sqff1o  27418  mpodvdsmulf1o  27430  dvdsmulf1o  27432  lgslem2  27534  lgslem3  27535  lgsfcl2  27539  rpvmasumlem  27723  dchrvmaeq0  27740  dchrisum0re  27749  pntlem3  27845  elleft  28116  elright  28117  elons  28518  elreno  28756  axcontlem2  29422  lfgredgge2  29581  uspgredg2vlem  29683  uspgredg2v  29684  usgredg2vlem1  29685  usgredg2vlem2  29686  ushgredgedg  29689  ushgredgedgloop  29691  uhgrspan1  29763  upgrreslem  29764  umgrreslem  29765  isfusgr  29778  nbupgrres  29824  nbusgredgeu0  29828  nbusgrf1o0  29829  uvtxel  29848  uvtxel1  29856  cusgrexilem2  29902  cusgrfilem2  29916  vtxdginducedm1lem4  30002  rgrx0ndm  30053  iswspthn  30317  wwlknon  30325  wspthnon  30326  wwlksn0  30331  wwlksnextfun  30366  wwlksnextinj  30367  wwlksnextsurj  30368  wwlksnextproplem3  30379  clwlkclwwlkflem  30474  clwlkclwwlkfolem  30477  isclwwlkn  30497  clwwlkel  30516  clwwlkf  30517  clwwlkf1  30519  isclwwlknon  30561  s2elclwwlknon2  30574  isfrgr  30740  frgrwopreglem3  30794  frgrwopreglem5lem  30800  frgrwopreglem5  30801  isablo  31027  iscbn  31345  hcau  31665  issh  31689  isch  31703  elcnop  32338  ellnop  32339  elbdop  32341  elhmop  32354  elcnfn  32363  ellnfn  32364  isst  32694  ishst  32695  ela  32820  isslmd  33642  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem4  33685  elrgspn  33686  ssmxidllem  33876  isufd  33950  iscref  34354  isrrext  34510  ispisys  34663  isldsys  34667  isros  34679  issros  34686  oddpwdc  34865  eulerpartleme  34874  eulerpartlemo  34876  eulerpartlemd  34877  eulerpartlemt0  34880  eulerpartlemf  34881  eulerpartlemt  34882  eulerpartlemr  34885  eulerpartlemmf  34886  eulerpartlemgvv  34887  eulerpartlemgs2  34891  eulerpartlemn  34892  elprob  34920  ballotlemelo  34999  ballotleme  35008  bnj1152  35507  bnj1280  35529  elscott  35624  elscott2  35627  elscottrank  35628  subfacp1lem3  35761  subfacp1lem5  35763  erdszelem1  35770  ispconn  35802  issconn  35805  cvmsiota  35856  cvmlift2lem12  35893  fmla1  35966  gonan0  35971  goaln0  35972  gonar  35974  goalr  35976  sategoelfvb  35998  rdgprc0  36370  elwlim  36400  neibastop1  36978  neibastop2lem  36979  neibastop2  36980  topdifinffinlem  38101  pibp19  38168  pibp21  38169  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  isprrngo  38800  rabeqel  39005  toycom  39846  isopos  40053  isoml  40111  isatl  40172  iscvlat  40196  ishlat1  40225  cdlemm10N  41991  dihglblem2N  42167  lcfl1lem  42364  lcfls1lem  42407  mapdordlem1a  42507  mapdordlem1  42509  iscsrg  42837  readvcot  43239  mhphflem  43442  pellqrex  43720  islnm  43918  pwssplit4  43930  islnr  43952  fnlimcnv  46495  stoweidlem14  46842  stoweidlem16  46844  stoweidlem37  46865  stoweidlem48  46876  stoweidlem51  46879  stoweidlem59  46887  salexct  47162  salexct2  47167  salexct3  47170  salgencntex  47171  salgensscntex  47172  ovn0lem  47393  opnvonmbllem1  47460  ovolval5lem2  47481  pimincfltioc  47544  pimdecfgtioo  47545  pimincfltioo  47546  smfresal  47616  smfmullem2  47620  smfpimbor1lem1  47626  smfpimbor1lem2  47627  smfinflem  47645  sprsymrelfo  48397  prproropf1olem1  48403  pairreueq  48410  iseven  48544  isodd  48545  m1expevenALTV  48563  iseven2  48567  isodd3  48568  odd2np1ALTV  48590  opoeALTV  48599  opeoALTV  48600  isgbe  48667  isgbow  48668  isgbo  48669  uspgrlimlem2  48905  uspgrlimlem3  48906  uspgrlimlem4  48907  clnbgrvtxedg  48910  grlimpredg  48914  grlimprclnbgrvtx  48915  grlimgrtrilem1  48917  0nodd  49085  1odd  49086  2nodd  49087  iscmgmALT  49139  issgrpALT  49140  iscsgrpALT  49141  1neven  49153  2zlidl  49155  2zrngamgm  49160  2zrngagrp  49164  2zrngmmgm  49167  2zrngnmrid  49171  isprmrng  49251  itsclc0  49701  itsclc0b  49702  isthinc  50345  istermc  50400