Theorem elrab2 3653

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440

This theorem is referenced by:  rru  3741  elrabsf  3790  fvmpti  6933  fvmptss2  6960  tfis  7795  elom  7809  oawordeulem  8479  oeeulem  8526  mapfienlem1  9314  mapfienlem3  9316  mapfien  9317  ordtypelem2  9430  ordtypelem3  9431  ordtypelem9  9437  wemapso2lem  9463  inf3lema  9539  oemapvali  9599  tz9.12lem3  9704  cofsmo  10182  enfin2i  10234  fin23lem28  10253  isf32lem6  10271  hsmexlem4  10342  zorn2lem2  10410  pwfseqlem1  10571  pwfseqlem3  10573  nqereu  10842  elz  12492  zsupss  12857  rpnnen1lem5  12901  elrp  12914  repos  13368  wwlktovf  14882  wwlktovf1  14883  wwlktovfo  14884  01sqrexlem1  15168  01sqrexlem2  15169  01sqrexlem6  15173  01sqrexlem7  15174  ello1  15441  elo1  15452  rlimrege0  15505  divalglem2  16325  divalglem4  16326  divalglem5  16327  divalglem9  16331  divalglem10  16332  bitsfzolem  16364  gcdcllem1  16429  gcdcllem2  16430  gcdcllem3  16431  bezoutlem1  16469  bezoutlem3  16471  bezoutlem4  16472  isprm  16603  maxprmfct  16639  phimullem  16709  eulerthlem1  16711  eulerthlem2  16712  hashgcdlem  16718  pclem  16769  pcprecl  16770  pcprendvds  16771  infpn2  16844  prmreclem1  16847  prmreclem2  16848  prmreclem3  16849  prmreclem5  16851  1arith  16858  elgz  16862  4sqlem13  16888  4sqlem17  16892  4sqlem18  16893  vdwnnlem2  16927  vdwnnlem3  16928  ramtlecl  16931  isdrs  18226  istos  18341  islat  18358  isclat  18425  isdlat  18447  istsr  18508  issgrp  18613  ismnddef  18629  gsumvallem2  18727  isgrp  18837  elnmz  19061  gastacl  19207  gastacos  19208  symgfixelq  19331  psgneldm  19401  sylow1lem2  19497  sylow1lem4  19499  sylow2alem1  19515  sylow2alem2  19516  efgsdm  19628  iscmn  19687  iscyg  19777  iscyggen  19778  dprdw  19910  ablfacrplem  19965  ablfacrp  19966  ablfac1c  19971  ablfac1eu  19973  pgpfaclem1  19981  ablfaclem3  19987  ablfac2  19989  issimpg  19992  isomnd  20021  isrng  20058  issrg  20092  isring  20141  iscrng  20144  isnzr  20418  islring  20444  isrrg  20602  isdomn  20609  isdrng  20637  isorng  20765  islmod  20786  islvec  21027  lspsolvlem  21068  lbsextlem1  21084  lbsextlem3  21086  lbsextlem4  21087  islpir  21254  isphl  21554  pjdm  21633  ishil  21644  frlmssuvc1  21720  frlmssuvc2  21721  frlmsslsp  21722  isassa  21782  psrbag  21843  psrbaglefi  21852  psrbagconcl  21853  psrbagleadd1  21854  gsumbagdiaglem  21856  mplelbas  21917  gsummatr01lem1  22559  gsummatr01lem4  22562  gsummatr01  22563  mretopd  22996  neipeltop  23033  isperf  23055  ist0  23224  ist1  23225  ishaus  23226  iscnrm  23227  isreg  23236  isnrm  23239  ispnrm  23243  iscmp  23292  hauscmplem  23310  isconn  23317  conncompss  23337  is1stc  23345  islly  23372  isnlly  23373  dfac14lem  23521  ishmeo  23663  ptcmplem3  23958  ptcmplem4  23959  istmd  23978  istgp  23981  tgpconncompeqg  24016  tgpt0  24023  qustgpopn  24024  istrg  24068  istdrg  24070  istlm  24089  istvc  24096  iscusp  24203  imasdsf1olem  24278  isxms  24352  isms  24354  blcld  24410  prdsxmslem2  24434  isngp  24501  isnrg  24565  isnlm  24580  icccmplem1  24728  icccmplem2  24729  isclm  24981  iscph  25087  isbn  25255  iscms  25262  ivthlem1  25369  ivthlem2  25370  ivthlem3  25371  elovolm  25393  ovolicc2lem2  25436  ovolicc2lem4  25438  ovolicc2lem5  25439  ismbl  25444  dyadmbllem  25517  dyadmbl  25518  ismbf1  25542  isi1f  25592  isibl  25683  isuc1p  26063  ismon1p  26065  radcnvle  26346  abelthlem2  26359  abelthlem7a  26364  atans  26857  lgamgulmlem2  26957  lgamgulmlem3  26958  lgamgulmlem5  26960  lgambdd  26964  wilthlem2  26996  wilthlem3  26997  ftalem3  27002  sqff1o  27109  mpodvdsmulf1o  27121  dvdsmulf1o  27123  lgslem2  27226  lgslem3  27227  lgsfcl2  27231  rpvmasumlem  27415  dchrvmaeq0  27432  dchrisum0re  27441  pntlem3  27537  elleft  27794  elright  27795  elons  28178  elreno  28383  axcontlem2  28929  lfgredgge2  29088  uspgredg2vlem  29187  uspgredg2v  29188  usgredg2vlem1  29189  usgredg2vlem2  29190  ushgredgedg  29193  ushgredgedgloop  29195  uhgrspan1  29267  upgrreslem  29268  umgrreslem  29269  isfusgr  29282  nbupgrres  29328  nbusgredgeu0  29332  nbusgrf1o0  29333  uvtxel  29352  uvtxel1  29360  cusgrexilem2  29406  cusgrfilem2  29421  vtxdginducedm1lem4  29507  rgrx0ndm  29558  iswspthn  29813  wwlknon  29821  wspthnon  29822  wwlksn0  29827  wwlksnextfun  29862  wwlksnextinj  29863  wwlksnextsurj  29864  wwlksnextproplem3  29875  clwlkclwwlkflem  29967  clwlkclwwlkfolem  29970  isclwwlkn  29990  clwwlkel  30009  clwwlkf  30010  clwwlkf1  30012  isclwwlknon  30054  s2elclwwlknon2  30067  isfrgr  30223  frgrwopreglem3  30277  frgrwopreglem5lem  30283  frgrwopreglem5  30284  isablo  30509  iscbn  30827  hcau  31147  issh  31171  isch  31185  elcnop  31820  ellnop  31821  elbdop  31823  elhmop  31836  elcnfn  31845  ellnfn  31846  isst  32176  ishst  32177  ela  32302  ischn  32967  isslmd  33163  elrgspnlem1  33201  elrgspnlem2  33202  elrgspnlem4  33204  elrgspn  33205  ssdifidllem  33412  ssdifidlprm  33414  ssmxidllem  33429  isufd  33496  iscref  33830  isrrext  33986  ispisys  34138  isldsys  34142  isros  34154  issros  34161  oddpwdc  34341  eulerpartleme  34350  eulerpartlemo  34352  eulerpartlemd  34353  eulerpartlemt0  34356  eulerpartlemf  34357  eulerpartlemt  34358  eulerpartlemr  34361  eulerpartlemmf  34362  eulerpartlemgvv  34363  eulerpartlemgs2  34367  eulerpartlemn  34368  elprob  34396  ballotlemelo  34475  ballotleme  34484  bnj1152  34984  bnj1280  35006  subfacp1lem3  35174  subfacp1lem5  35176  erdszelem1  35183  ispconn  35215  issconn  35218  cvmsiota  35269  cvmlift2lem12  35306  fmla1  35379  gonan0  35384  goaln0  35385  gonar  35387  goalr  35389  sategoelfvb  35411  rdgprc0  35786  elwlim  35816  neibastop1  36352  neibastop2lem  36353  neibastop2  36354  topdifinffinlem  37340  pibp19  37407  pibp21  37408  poimirlem5  37624  poimirlem6  37625  poimirlem7  37626  poimirlem8  37627  poimirlem10  37629  poimirlem11  37630  poimirlem12  37631  poimirlem15  37634  poimirlem16  37635  poimirlem17  37636  poimirlem18  37637  poimirlem19  37638  poimirlem20  37639  poimirlem21  37640  poimirlem22  37641  isprrngo  38049  rabeqel  38248  toycom  38971  isopos  39178  isoml  39236  isatl  39297  iscvlat  39321  ishlat1  39350  cdlemm10N  41117  dihglblem2N  41293  lcfl1lem  41490  lcfls1lem  41533  mapdordlem1a  41633  mapdordlem1  41635  iscsrg  41963  readvcot  42357  mhphflem  42589  pellqrex  42872  islnm  43070  pwssplit4  43082  islnr  43104  fnlimcnv  45668  stoweidlem14  46015  stoweidlem16  46017  stoweidlem37  46038  stoweidlem48  46049  stoweidlem51  46052  stoweidlem59  46060  salexct  46335  salexct2  46340  salexct3  46343  salgencntex  46344  salgensscntex  46345  ovn0lem  46566  opnvonmbllem1  46633  ovolval5lem2  46654  pimincfltioc  46717  pimdecfgtioo  46718  pimincfltioo  46719  smfresal  46789  smfmullem2  46793  smfpimbor1lem1  46799  smfpimbor1lem2  46800  smfinflem  46818  sprsymrelfo  47501  prproropf1olem1  47507  pairreueq  47514  iseven  47632  isodd  47633  m1expevenALTV  47651  iseven2  47655  isodd3  47656  odd2np1ALTV  47678  opoeALTV  47687  opeoALTV  47688  isgbe  47755  isgbow  47756  isgbo  47757  uspgrlimlem2  47993  uspgrlimlem3  47994  uspgrlimlem4  47995  clnbgrvtxedg  47998  grlimpredg  48002  grlimprclnbgrvtx  48003  grlimgrtrilem1  48005  0nodd  48174  1odd  48175  2nodd  48176  iscmgmALT  48228  issgrpALT  48229  iscsgrpALT  48230  1neven  48242  2zlidl  48244  2zrngamgm  48249  2zrngagrp  48253  2zrngmmgm  48256  2zrngnmrid  48260  itsclc0  48776  itsclc0b  48777  isthinc  49424  istermc  49479