Theorem elrab2 3620

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424

This theorem is referenced by:  rru  3709  elrabsf  3759  fvmpti  6856  fvmptss2  6882  tfis  7676  elom  7690  oawordeulem  8347  oeeulem  8394  mapfienlem1  9094  mapfienlem3  9096  mapfien  9097  ordtypelem2  9208  ordtypelem3  9209  ordtypelem9  9215  wemapso2lem  9241  inf3lema  9312  oemapvali  9372  tz9.12lem3  9478  cofsmo  9956  enfin2i  10008  fin23lem28  10027  isf32lem6  10045  hsmexlem4  10116  zorn2lem2  10184  pwfseqlem1  10345  pwfseqlem3  10347  nqereu  10616  elz  12251  zsupss  12606  rpnnen1lem5  12650  elrp  12661  repos  13107  wwlktovf  14599  wwlktovf1  14600  wwlktovfo  14601  sqrlem1  14882  sqrlem2  14883  sqrlem6  14887  sqrlem7  14888  ello1  15152  elo1  15163  rlimrege0  15216  divalglem2  16032  divalglem4  16033  divalglem5  16034  divalglem9  16038  divalglem10  16039  bitsfzolem  16069  gcdcllem1  16134  gcdcllem2  16135  gcdcllem3  16136  bezoutlem1  16175  bezoutlem3  16177  bezoutlem4  16178  isprm  16306  maxprmfct  16342  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  hashgcdlem  16417  pclem  16467  pcprecl  16468  pcprendvds  16469  infpn2  16542  prmreclem1  16545  prmreclem2  16546  prmreclem3  16547  prmreclem5  16549  1arith  16556  elgz  16560  4sqlem13  16586  4sqlem17  16590  4sqlem18  16591  vdwnnlem2  16625  vdwnnlem3  16626  ramtlecl  16629  isdrs  17934  istos  18051  islat  18066  isclat  18133  isdlat  18155  istsr  18216  issgrp  18291  ismnddef  18302  gsumvallem2  18387  isgrp  18498  elnmz  18706  gastacl  18830  gastacos  18831  symgfixelq  18956  psgneldm  19026  sylow1lem2  19119  sylow1lem4  19121  sylow2alem1  19137  sylow2alem2  19138  efgsdm  19251  iscmn  19309  iscyg  19394  iscyggen  19395  dprdw  19528  ablfacrplem  19583  ablfacrp  19584  ablfac1c  19589  ablfac1eu  19591  pgpfaclem1  19599  ablfaclem3  19605  ablfac2  19607  issimpg  19610  issrg  19658  isring  19702  iscrng  19705  isdrng  19910  islmod  20042  islvec  20281  lspsolvlem  20319  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  islpir  20433  isnzr  20443  isrrg  20472  isdomn  20478  isphl  20745  pjdm  20824  ishil  20835  frlmssuvc1  20911  frlmssuvc2  20912  frlmsslsp  20913  isassa  20973  psrbag  21030  psrbaglefi  21045  psrbaglefiOLD  21046  psrbagconcl  21047  psrbagconclOLD  21048  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  mplelbas  21109  gsummatr01lem1  21712  gsummatr01lem4  21715  gsummatr01  21716  mretopd  22151  neipeltop  22188  isperf  22210  ist0  22379  ist1  22380  ishaus  22381  iscnrm  22382  isreg  22391  isnrm  22394  ispnrm  22398  iscmp  22447  hauscmplem  22465  isconn  22472  conncompss  22492  is1stc  22500  islly  22527  isnlly  22528  dfac14lem  22676  ishmeo  22818  ptcmplem3  23113  ptcmplem4  23114  istmd  23133  istgp  23136  tgpconncompeqg  23171  tgpt0  23178  qustgpopn  23179  istrg  23223  istdrg  23225  istlm  23244  istvc  23251  iscusp  23359  imasdsf1olem  23434  isxms  23508  isms  23510  blcld  23567  prdsxmslem2  23591  isngp  23658  isnrg  23730  isnlm  23745  icccmplem1  23891  icccmplem2  23892  isclm  24133  iscph  24239  isbn  24407  iscms  24414  ivthlem1  24520  ivthlem2  24521  ivthlem3  24522  elovolm  24544  ovolicc2lem2  24587  ovolicc2lem4  24589  ovolicc2lem5  24590  ismbl  24595  dyadmbllem  24668  dyadmbl  24669  ismbf1  24693  isi1f  24743  isibl  24835  isuc1p  25210  ismon1p  25212  radcnvle  25484  abelthlem2  25496  abelthlem7a  25501  atans  25985  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgambdd  26091  wilthlem2  26123  wilthlem3  26124  ftalem3  26129  sqff1o  26236  dvdsmulf1o  26248  lgslem2  26351  lgslem3  26352  lgsfcl2  26356  rpvmasumlem  26540  dchrvmaeq0  26557  dchrisum0re  26566  pntlem3  26662  axcontlem2  27236  lfgredgge2  27397  uspgredg2vlem  27493  uspgredg2v  27494  usgredg2vlem1  27495  usgredg2vlem2  27496  ushgredgedg  27499  ushgredgedgloop  27501  uhgrspan1  27573  upgrreslem  27574  umgrreslem  27575  isfusgr  27588  nbupgrres  27634  nbusgredgeu0  27638  nbusgrf1o0  27639  uvtxel  27658  uvtxel1  27666  cusgrexilem2  27712  cusgrfilem2  27726  vtxdginducedm1lem4  27812  rgrx0ndm  27863  iswspthn  28115  wwlknon  28123  wspthnon  28124  wwlksn0  28129  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextsurj  28166  wwlksnextproplem3  28177  clwlkclwwlkflem  28269  clwlkclwwlkfolem  28272  isclwwlkn  28292  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  isclwwlknon  28356  s2elclwwlknon2  28369  isfrgr  28525  frgrwopreglem3  28579  frgrwopreglem5lem  28585  frgrwopreglem5  28586  isablo  28809  iscbn  29127  hcau  29447  issh  29471  isch  29485  elcnop  30120  ellnop  30121  elbdop  30123  elhmop  30136  elcnfn  30145  ellnfn  30146  isst  30476  ishst  30477  ela  30602  isomnd  31229  isslmd  31357  isorng  31400  ssmxidllem  31543  isufd  31565  iscref  31696  isrrext  31850  ispisys  32020  isldsys  32024  isros  32036  issros  32043  oddpwdc  32221  eulerpartleme  32230  eulerpartlemo  32232  eulerpartlemd  32233  eulerpartlemt0  32236  eulerpartlemf  32237  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgs2  32247  eulerpartlemn  32248  elprob  32276  ballotlemelo  32354  ballotleme  32363  bnj1152  32878  bnj1280  32900  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem1  33053  ispconn  33085  issconn  33088  cvmsiota  33139  cvmlift2lem12  33176  fmla1  33249  gonan0  33254  goaln0  33255  gonar  33257  goalr  33259  sategoelfvb  33281  rdgprc0  33675  elwlim  33744  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  topdifinffinlem  35445  pibp19  35512  pibp21  35513  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  isprrngo  36135  rabeqel  36321  toycom  36914  isopos  37121  isoml  37179  isatl  37240  iscvlat  37264  ishlat1  37293  cdlemm10N  39059  dihglblem2N  39235  lcfl1lem  39432  lcfls1lem  39475  mapdordlem1a  39575  mapdordlem1  39577  mhphflem  40207  pellqrex  40617  islnm  40818  pwssplit4  40830  islnr  40852  fnlimcnv  43098  stoweidlem14  43445  stoweidlem16  43447  stoweidlem37  43468  stoweidlem48  43479  stoweidlem51  43482  stoweidlem59  43490  salexct  43763  salexct2  43768  salexct3  43771  salgencntex  43772  salgensscntex  43773  ovn0lem  43993  opnvonmbllem1  44060  ovolval5lem2  44081  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  smfresal  44209  smfmullem2  44213  smfpimbor1lem1  44219  smfpimbor1lem2  44220  smfinflem  44237  sprsymrelfo  44837  prproropf1olem1  44843  pairreueq  44850  iseven  44968  isodd  44969  m1expevenALTV  44987  iseven2  44991  isodd3  44992  odd2np1ALTV  45014  opoeALTV  45023  opeoALTV  45024  isgbe  45091  isgbow  45092  isgbo  45093  0nodd  45252  1odd  45253  2nodd  45254  iscmgmALT  45306  issgrpALT  45307  iscsgrpALT  45308  isrng  45322  1neven  45378  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  2zrngnmrid  45396  itsclc0  46005  itsclc0b  46006  isthinc  46190