Theorem elrab2 3711

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490

This theorem is referenced by:  rru  3801  elrabsf  3853  fvmpti  7028  fvmptss2  7055  tfis  7892  elom  7906  oawordeulem  8610  oeeulem  8657  mapfienlem1  9474  mapfienlem3  9476  mapfien  9477  ordtypelem2  9588  ordtypelem3  9589  ordtypelem9  9595  wemapso2lem  9621  inf3lema  9693  oemapvali  9753  tz9.12lem3  9858  cofsmo  10338  enfin2i  10390  fin23lem28  10409  isf32lem6  10427  hsmexlem4  10498  zorn2lem2  10566  pwfseqlem1  10727  pwfseqlem3  10729  nqereu  10998  elz  12641  zsupss  13002  rpnnen1lem5  13046  elrp  13059  repos  13506  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  01sqrexlem1  15291  01sqrexlem2  15292  01sqrexlem6  15296  01sqrexlem7  15297  ello1  15561  elo1  15572  rlimrege0  15625  divalglem2  16443  divalglem4  16444  divalglem5  16445  divalglem9  16449  divalglem10  16450  bitsfzolem  16480  gcdcllem1  16545  gcdcllem2  16546  gcdcllem3  16547  bezoutlem1  16586  bezoutlem3  16588  bezoutlem4  16589  isprm  16720  maxprmfct  16756  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  hashgcdlem  16835  pclem  16885  pcprecl  16886  pcprendvds  16887  infpn2  16960  prmreclem1  16963  prmreclem2  16964  prmreclem3  16965  prmreclem5  16967  1arith  16974  elgz  16978  4sqlem13  17004  4sqlem17  17008  4sqlem18  17009  vdwnnlem2  17043  vdwnnlem3  17044  ramtlecl  17047  isdrs  18371  istos  18488  islat  18503  isclat  18570  isdlat  18592  istsr  18653  issgrp  18758  ismnddef  18774  gsumvallem2  18869  isgrp  18979  elnmz  19203  gastacl  19349  gastacos  19350  symgfixelq  19475  psgneldm  19545  sylow1lem2  19641  sylow1lem4  19643  sylow2alem1  19659  sylow2alem2  19660  efgsdm  19772  iscmn  19831  iscyg  19921  iscyggen  19922  dprdw  20054  ablfacrplem  20109  ablfacrp  20110  ablfac1c  20115  ablfac1eu  20117  pgpfaclem1  20125  ablfaclem3  20131  ablfac2  20133  issimpg  20136  isrng  20181  issrg  20215  isring  20264  iscrng  20267  isnzr  20540  islring  20566  isrrg  20720  isdomn  20727  isdrng  20755  islmod  20884  islvec  21126  lspsolvlem  21167  lbsextlem1  21183  lbsextlem3  21185  lbsextlem4  21186  islpir  21361  isphl  21669  pjdm  21750  ishil  21761  frlmssuvc1  21837  frlmssuvc2  21838  frlmsslsp  21839  isassa  21899  psrbag  21960  psrbaglefi  21969  psrbagconcl  21970  psrbagleadd1  21971  gsumbagdiaglem  21973  mplelbas  22034  gsummatr01lem1  22682  gsummatr01lem4  22685  gsummatr01  22686  mretopd  23121  neipeltop  23158  isperf  23180  ist0  23349  ist1  23350  ishaus  23351  iscnrm  23352  isreg  23361  isnrm  23364  ispnrm  23368  iscmp  23417  hauscmplem  23435  isconn  23442  conncompss  23462  is1stc  23470  islly  23497  isnlly  23498  dfac14lem  23646  ishmeo  23788  ptcmplem3  24083  ptcmplem4  24084  istmd  24103  istgp  24106  tgpconncompeqg  24141  tgpt0  24148  qustgpopn  24149  istrg  24193  istdrg  24195  istlm  24214  istvc  24221  iscusp  24329  imasdsf1olem  24404  isxms  24478  isms  24480  blcld  24539  prdsxmslem2  24563  isngp  24630  isnrg  24702  isnlm  24717  icccmplem1  24863  icccmplem2  24864  isclm  25116  iscph  25223  isbn  25391  iscms  25398  ivthlem1  25505  ivthlem2  25506  ivthlem3  25507  elovolm  25529  ovolicc2lem2  25572  ovolicc2lem4  25574  ovolicc2lem5  25575  ismbl  25580  dyadmbllem  25653  dyadmbl  25654  ismbf1  25678  isi1f  25728  isibl  25820  isuc1p  26200  ismon1p  26202  radcnvle  26481  abelthlem2  26494  abelthlem7a  26499  atans  26991  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgambdd  27098  wilthlem2  27130  wilthlem3  27131  ftalem3  27136  sqff1o  27243  mpodvdsmulf1o  27255  dvdsmulf1o  27257  lgslem2  27360  lgslem3  27361  lgsfcl2  27365  rpvmasumlem  27549  dchrvmaeq0  27566  dchrisum0re  27575  pntlem3  27671  0elleft  27966  0elright  27967  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  negsproplem4  28081  negsproplem5  28082  mulsproplem12  28171  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  elons  28294  sltonold  28301  elreno  28445  axcontlem2  28998  lfgredgge2  29159  uspgredg2vlem  29258  uspgredg2v  29259  usgredg2vlem1  29260  usgredg2vlem2  29261  ushgredgedg  29264  ushgredgedgloop  29266  uhgrspan1  29338  upgrreslem  29339  umgrreslem  29340  isfusgr  29353  nbupgrres  29399  nbusgredgeu0  29403  nbusgrf1o0  29404  uvtxel  29423  uvtxel1  29431  cusgrexilem2  29477  cusgrfilem2  29492  vtxdginducedm1lem4  29578  rgrx0ndm  29629  iswspthn  29882  wwlknon  29890  wspthnon  29891  wwlksn0  29896  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextsurj  29933  wwlksnextproplem3  29944  clwlkclwwlkflem  30036  clwlkclwwlkfolem  30039  isclwwlkn  30059  clwwlkel  30078  clwwlkf  30079  clwwlkf1  30081  isclwwlknon  30123  s2elclwwlknon2  30136  isfrgr  30292  frgrwopreglem3  30346  frgrwopreglem5lem  30352  frgrwopreglem5  30353  isablo  30578  iscbn  30896  hcau  31216  issh  31240  isch  31254  elcnop  31889  ellnop  31890  elbdop  31892  elhmop  31905  elcnfn  31914  ellnfn  31915  isst  32245  ishst  32246  ela  32371  ischn  32979  isomnd  33051  isslmd  33181  isorng  33294  ssdifidllem  33449  ssdifidlprm  33451  ssmxidllem  33466  isufd  33533  iscref  33790  isrrext  33946  ispisys  34116  isldsys  34120  isros  34132  issros  34139  oddpwdc  34319  eulerpartleme  34328  eulerpartlemo  34330  eulerpartlemd  34331  eulerpartlemt0  34334  eulerpartlemf  34335  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgs2  34345  eulerpartlemn  34346  elprob  34374  ballotlemelo  34452  ballotleme  34461  bnj1152  34974  bnj1280  34996  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem1  35159  ispconn  35191  issconn  35194  cvmsiota  35245  cvmlift2lem12  35282  fmla1  35355  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  sategoelfvb  35387  rdgprc0  35757  elwlim  35787  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  topdifinffinlem  37313  pibp19  37380  pibp21  37381  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  isprrngo  38010  rabeqel  38210  toycom  38929  isopos  39136  isoml  39194  isatl  39255  iscvlat  39279  ishlat1  39308  cdlemm10N  41075  dihglblem2N  41251  lcfl1lem  41448  lcfls1lem  41491  mapdordlem1a  41591  mapdordlem1  41593  iscsrg  41925  mhphflem  42551  pellqrex  42835  islnm  43034  pwssplit4  43046  islnr  43068  fnlimcnv  45588  stoweidlem14  45935  stoweidlem16  45937  stoweidlem37  45958  stoweidlem48  45969  stoweidlem51  45972  stoweidlem59  45980  salexct  46255  salexct2  46260  salexct3  46263  salgencntex  46264  salgensscntex  46265  ovn0lem  46486  opnvonmbllem1  46553  ovolval5lem2  46574  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  smfresal  46709  smfmullem2  46713  smfpimbor1lem1  46719  smfpimbor1lem2  46720  smfinflem  46738  sprsymrelfo  47371  prproropf1olem1  47377  pairreueq  47384  iseven  47502  isodd  47503  m1expevenALTV  47521  iseven2  47525  isodd3  47526  odd2np1ALTV  47548  opoeALTV  47557  opeoALTV  47558  isgbe  47625  isgbow  47626  isgbo  47627  uspgrlimlem2  47813  uspgrlimlem3  47814  uspgrlimlem4  47815  0nodd  47893  1odd  47894  2nodd  47895  iscmgmALT  47947  issgrpALT  47948  iscsgrpALT  47949  1neven  47961  2zlidl  47963  2zrngamgm  47968  2zrngagrp  47972  2zrngmmgm  47975  2zrngnmrid  47979  itsclc0  48505  itsclc0b  48506  isthinc  48688