Theorem elrab2 3654

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457

This theorem is referenced by:  rru  3742  elrabsf  3789  fvmpti  6988  fvmptss2  7016  tfis  7847  elom  7861  oawordeulem  8535  oeeulem  8583  mapfienlem1  9361  mapfienlem3  9363  mapfien  9364  ordtypelem2  9477  ordtypelem3  9478  ordtypelem9  9484  wemapso2lem  9510  inf3lema  9589  oemapvali  9649  tz9.12lem3  9757  cofsmo  10248  enfin2i  10300  fin23lem28  10319  isf32lem6  10337  hsmexlem4  10408  zorn2lem2  10476  pwfseqlem1  10638  pwfseqlem3  10640  nqereu  10909  elz  12588  zsupss  12956  rpnnen1lem5  13000  elrp  13013  repos  13468  wwlktovf  14989  wwlktovf1  14990  wwlktovfo  14991  01sqrexlem1  15289  01sqrexlem2  15290  01sqrexlem6  15294  01sqrexlem7  15295  ello1  15562  elo1  15573  rlimrege0  15626  divalglem2  16448  divalglem4  16449  divalglem5  16450  divalglem9  16454  divalglem10  16455  bitsfzolem  16487  gcdcllem1  16552  gcdcllem2  16553  gcdcllem3  16554  bezoutlem1  16592  bezoutlem3  16594  bezoutlem4  16595  isprm  16726  maxprmfct  16763  phimullem  16833  eulerthlem1  16835  eulerthlem2  16836  hashgcdlem  16842  pclem  16893  pcprecl  16894  pcprendvds  16895  infpn2  16968  prmreclem1  16971  prmreclem2  16972  prmreclem3  16973  prmreclem5  16975  1arith  16982  elgz  16986  4sqlem13  17012  4sqlem17  17016  4sqlem18  17017  vdwnnlem2  17051  vdwnnlem3  17052  ramtlecl  17055  isdrs  18352  istos  18467  islat  18484  isclat  18551  isdlat  18573  istsr  18634  ischn  18658  issgrp  18773  ismnddef  18789  gsumvallem2  18888  isgrp  19001  elnmz  19224  gastacl  19374  gastacos  19375  symgfixelq  19498  psgneldm  19568  sylow1lem2  19664  sylow1lem4  19666  sylow2alem1  19682  sylow2alem2  19683  efgsdm  19795  iscmn  19854  iscyg  19944  iscyggen  19945  dprdw  20077  ablfacrplem  20132  ablfacrp  20133  ablfac1c  20138  ablfac1eu  20140  pgpfaclem1  20148  ablfaclem3  20154  ablfac2  20156  issimpg  20159  isomnd  20188  isrng  20227  issrg  20265  isring  20314  iscrng  20317  isnzr  20611  islring  20639  isrrg  20797  isdomn  20804  isdrng  20831  isorng  20964  islmod  20985  islvec  21225  lspsolvlem  21266  lbsextlem1  21282  lbsextlem3  21284  lbsextlem4  21285  ssdifidllem  21484  ssdifidlprm  21486  islpir  21496  isphl  21778  pjdm  21857  ishil  21868  frlmssuvc1  21944  frlmssuvc2  21945  frlmsslsp  21946  isassa  22006  psrbag  22067  psrbaglefi  22076  psrbagconcl  22077  psrbagleadd1  22078  gsumbagdiaglem  22081  mplelbas  22140  gsummatr01lem1  22812  gsummatr01lem4  22815  gsummatr01  22816  mretopd  23249  neipeltop  23286  isperf  23308  ist0  23477  ist1  23478  ishaus  23479  iscnrm  23480  isreg  23489  isnrm  23492  ispnrm  23496  iscmp  23545  hauscmplem  23563  isconn  23570  conncompss  23590  is1stc  23598  islly  23625  isnlly  23626  dfac14lem  23774  ishmeo  23916  ptcmplem3  24211  ptcmplem4  24212  istmd  24231  istgp  24234  tgpconncompeqg  24269  tgpt0  24276  qustgpopn  24277  istrg  24321  istdrg  24323  istlm  24342  istvc  24349  iscusp  24455  imasdsf1olem  24530  isxms  24604  isms  24606  blcld  24662  prdsxmslem2  24686  isngp  24753  isnrg  24817  isnlm  24832  icccmplem1  24980  icccmplem2  24981  isclm  25223  iscph  25329  isbn  25497  iscms  25504  ivthlem1  25610  ivthlem2  25611  ivthlem3  25612  elovolm  25634  ovolicc2lem2  25677  ovolicc2lem4  25679  ovolicc2lem5  25680  ismbl  25685  dyadmbllem  25758  dyadmbl  25759  ismbf1  25783  isi1f  25833  isibl  25924  isuc1p  26298  ismon1p  26300  radcnvle  26583  abelthlem2  26595  abelthlem7a  26600  atans  27095  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgambdd  27201  wilthlem2  27233  wilthlem3  27234  ftalem3  27239  sqff1o  27346  mpodvdsmulf1o  27358  dvdsmulf1o  27360  lgslem2  27462  lgslem3  27463  lgsfcl2  27467  rpvmasumlem  27651  dchrvmaeq0  27668  dchrisum0re  27677  pntlem3  27773  elleft  28044  elright  28045  elons  28446  elreno  28684  axcontlem2  29315  lfgredgge2  29474  uspgredg2vlem  29573  uspgredg2v  29574  usgredg2vlem1  29575  usgredg2vlem2  29576  ushgredgedg  29579  ushgredgedgloop  29581  uhgrspan1  29653  upgrreslem  29654  umgrreslem  29655  isfusgr  29668  nbupgrres  29714  nbusgredgeu0  29718  nbusgrf1o0  29719  uvtxel  29738  uvtxel1  29746  cusgrexilem2  29792  cusgrfilem2  29806  vtxdginducedm1lem4  29892  rgrx0ndm  29943  iswspthn  30198  wwlknon  30206  wspthnon  30207  wwlksn0  30212  wwlksnextfun  30247  wwlksnextinj  30248  wwlksnextsurj  30249  wwlksnextproplem3  30260  clwlkclwwlkflem  30355  clwlkclwwlkfolem  30358  isclwwlkn  30378  clwwlkel  30397  clwwlkf  30398  clwwlkf1  30400  isclwwlknon  30442  s2elclwwlknon2  30455  isfrgr  30611  frgrwopreglem3  30665  frgrwopreglem5lem  30671  frgrwopreglem5  30672  isablo  30898  iscbn  31216  hcau  31536  issh  31560  isch  31574  elcnop  32209  ellnop  32210  elbdop  32212  elhmop  32225  elcnfn  32234  ellnfn  32235  isst  32565  ishst  32566  ela  32691  isslmd  33522  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem4  33565  elrgspn  33566  ssmxidllem  33756  isufd  33830  iscref  34234  isrrext  34390  ispisys  34542  isldsys  34546  isros  34558  issros  34565  oddpwdc  34744  eulerpartleme  34753  eulerpartlemo  34755  eulerpartlemd  34756  eulerpartlemt0  34759  eulerpartlemf  34760  eulerpartlemt  34761  eulerpartlemr  34764  eulerpartlemmf  34765  eulerpartlemgvv  34766  eulerpartlemgs2  34770  eulerpartlemn  34771  elprob  34799  ballotlemelo  34878  ballotleme  34887  bnj1152  35386  bnj1280  35408  elscott  35510  elscott2  35513  elscottrank  35514  subfacp1lem3  35674  subfacp1lem5  35676  erdszelem1  35683  ispconn  35715  issconn  35718  cvmsiota  35769  cvmlift2lem12  35806  fmla1  35879  gonan0  35884  goaln0  35885  gonar  35887  goalr  35889  sategoelfvb  35911  rdgprc0  36283  elwlim  36313  neibastop1  36870  neibastop2lem  36871  neibastop2  36872  topdifinffinlem  37993  pibp19  38060  pibp21  38061  poimirlem5  38276  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem10  38281  poimirlem11  38282  poimirlem12  38283  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem18  38289  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  isprrngo  38701  rabeqel  38906  toycom  39747  isopos  39954  isoml  40012  isatl  40073  iscvlat  40097  ishlat1  40126  cdlemm10N  41892  dihglblem2N  42068  lcfl1lem  42265  lcfls1lem  42308  mapdordlem1a  42408  mapdordlem1  42410  iscsrg  42738  readvcot  43125  mhphflem  43328  pellqrex  43606  islnm  43804  pwssplit4  43816  islnr  43838  fnlimcnv  46381  stoweidlem14  46728  stoweidlem16  46730  stoweidlem37  46751  stoweidlem48  46762  stoweidlem51  46765  stoweidlem59  46773  salexct  47048  salexct2  47053  salexct3  47056  salgencntex  47057  salgensscntex  47058  ovn0lem  47279  opnvonmbllem1  47346  ovolval5lem2  47367  pimincfltioc  47430  pimdecfgtioo  47431  pimincfltioo  47432  smfresal  47502  smfmullem2  47506  smfpimbor1lem1  47512  smfpimbor1lem2  47513  smfinflem  47531  sprsymrelfo  48246  prproropf1olem1  48252  pairreueq  48259  iseven  48393  isodd  48394  m1expevenALTV  48412  iseven2  48416  isodd3  48417  odd2np1ALTV  48439  opoeALTV  48448  opeoALTV  48449  isgbe  48516  isgbow  48517  isgbo  48518  uspgrlimlem2  48754  uspgrlimlem3  48755  uspgrlimlem4  48756  clnbgrvtxedg  48759  grlimpredg  48763  grlimprclnbgrvtx  48764  grlimgrtrilem1  48766  0nodd  48935  1odd  48936  2nodd  48937  iscmgmALT  48989  issgrpALT  48990  iscsgrpALT  48991  1neven  49003  2zlidl  49005  2zrngamgm  49010  2zrngagrp  49014  2zrngmmgm  49017  2zrngnmrid  49021  isprmrng  49101  itsclc0  49551  itsclc0b  49552  isthinc  50197  istermc  50252