Theorem elrab2 3683

Description: Membership in a 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 2904	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3680	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 277	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496

This theorem is referenced by:  rru  3770  elrabsf  3816  fvmpti  6767  fvmptss2  6793  tfis  7569  elom  7583  oawordeulem  8180  oeeulem  8227  mapfienlem1  8868  mapfienlem3  8870  mapfien  8871  ordtypelem2  8983  ordtypelem3  8984  ordtypelem9  8990  wemapso2lem  9016  inf3lema  9087  oemapvali  9147  tz9.12lem3  9218  cofsmo  9691  enfin2i  9743  fin23lem28  9762  isf32lem6  9780  hsmexlem4  9851  zorn2lem2  9919  pwfseqlem1  10080  pwfseqlem3  10082  nqereu  10351  elz  11984  zsupss  12338  rpnnen1lem5  12381  elrp  12392  repos  12835  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  sqrlem1  14602  sqrlem2  14603  sqrlem6  14607  sqrlem7  14608  ello1  14872  elo1  14883  rlimrege0  14936  divalglem2  15746  divalglem4  15747  divalglem5  15748  divalglem9  15752  divalglem10  15753  bitsfzolem  15783  gcdcllem1  15848  gcdcllem2  15849  gcdcllem3  15850  bezoutlem1  15887  bezoutlem3  15889  bezoutlem4  15890  isprm  16017  maxprmfct  16053  phimullem  16116  eulerthlem1  16118  eulerthlem2  16119  hashgcdlem  16125  pclem  16175  pcprecl  16176  pcprendvds  16177  infpn2  16249  prmreclem1  16252  prmreclem2  16253  prmreclem3  16254  prmreclem5  16256  1arith  16263  elgz  16267  4sqlem13  16293  4sqlem17  16297  4sqlem18  16298  vdwnnlem2  16332  vdwnnlem3  16333  ramtlecl  16336  isdrs  17544  istos  17645  islat  17657  isclat  17719  isdlat  17803  istsr  17827  issgrp  17902  ismnddef  17913  gsumvallem2  17998  isgrp  18109  elnmz  18315  gastacl  18439  gastacos  18440  symgfixelq  18561  psgneldm  18631  sylow1lem2  18724  sylow1lem4  18726  sylow2alem1  18742  sylow2alem2  18743  efgsdm  18856  iscmn  18914  iscyg  18998  iscyggen  18999  dprdw  19132  ablfacrplem  19187  ablfacrp  19188  ablfac1c  19193  ablfac1eu  19195  pgpfaclem1  19203  ablfaclem3  19209  ablfac2  19211  issimpg  19214  issrg  19257  isring  19301  iscrng  19304  isdrng  19506  islmod  19638  islvec  19876  lspsolvlem  19914  lbsextlem1  19930  lbsextlem3  19932  lbsextlem4  19933  islpir  20022  isnzr  20032  isrrg  20061  isdomn  20067  isassa  20088  psrbag  20144  psrbaglefi  20152  psrbagconcl  20153  psrbagconf1o  20154  gsumbagdiaglem  20155  mplelbas  20210  isphl  20772  pjdm  20851  ishil  20862  frlmssuvc1  20938  frlmssuvc2  20939  frlmsslsp  20940  gsummatr01lem1  21264  gsummatr01lem4  21267  gsummatr01  21268  mretopd  21700  neipeltop  21737  isperf  21759  ist0  21928  ist1  21929  ishaus  21930  iscnrm  21931  isreg  21940  isnrm  21943  ispnrm  21947  iscmp  21996  hauscmplem  22014  isconn  22021  conncompss  22041  is1stc  22049  islly  22076  isnlly  22077  dfac14lem  22225  ishmeo  22367  ptcmplem3  22662  ptcmplem4  22663  istmd  22682  istgp  22685  tgpconncompeqg  22720  tgpt0  22727  qustgpopn  22728  istrg  22772  istdrg  22774  istlm  22793  istvc  22800  iscusp  22908  imasdsf1olem  22983  isxms  23057  isms  23059  blcld  23115  prdsxmslem2  23139  isngp  23205  isnrg  23269  isnlm  23284  icccmplem1  23430  icccmplem2  23431  isclm  23668  iscph  23774  isbn  23941  iscms  23948  ivthlem1  24052  ivthlem2  24053  ivthlem3  24054  elovolm  24076  ovolicc2lem2  24119  ovolicc2lem4  24121  ovolicc2lem5  24122  ismbl  24127  dyadmbllem  24200  dyadmbl  24201  ismbf1  24225  isi1f  24275  isibl  24366  isuc1p  24734  ismon1p  24736  radcnvle  25008  abelthlem2  25020  abelthlem7a  25025  atans  25508  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  wilthlem2  25646  wilthlem3  25647  ftalem3  25652  sqff1o  25759  dvdsmulf1o  25771  lgslem2  25874  lgslem3  25875  lgsfcl2  25879  rpvmasumlem  26063  dchrvmaeq0  26080  dchrisum0re  26089  pntlem3  26185  axcontlem2  26751  lfgredgge2  26909  uspgredg2vlem  27005  uspgredg2v  27006  usgredg2vlem1  27007  usgredg2vlem2  27008  ushgredgedg  27011  ushgredgedgloop  27013  uhgrspan1  27085  upgrreslem  27086  umgrreslem  27087  isfusgr  27100  nbupgrres  27146  nbusgredgeu0  27150  nbusgrf1o0  27151  uvtxel  27170  uvtxel1  27178  cusgrexilem2  27224  cusgrfilem2  27238  vtxdginducedm1lem4  27324  rgrx0ndm  27375  iswspthn  27627  wwlknon  27635  wspthnon  27636  wwlksn0  27641  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextsurj  27678  wwlksnextproplem3  27690  clwlkclwwlkflem  27782  clwlkclwwlkfolem  27785  isclwwlkn  27805  clwwlkel  27825  clwwlkf  27826  clwwlkf1  27828  isclwwlknon  27870  s2elclwwlknon2  27883  isfrgr  28039  frgrwopreglem3  28093  frgrwopreglem5lem  28099  frgrwopreglem5  28100  isablo  28323  iscbn  28641  hcau  28961  issh  28985  isch  28999  elcnop  29634  ellnop  29635  elbdop  29637  elhmop  29650  elcnfn  29659  ellnfn  29660  isst  29990  ishst  29991  ela  30116  isomnd  30702  isslmd  30830  isorng  30872  ssmxidllem  30978  iscref  31108  isrrext  31241  ispisys  31411  isldsys  31415  isros  31427  issros  31434  oddpwdc  31612  eulerpartleme  31621  eulerpartlemo  31623  eulerpartlemd  31624  eulerpartlemt0  31627  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartlemr  31632  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgs2  31638  eulerpartlemn  31639  elprob  31667  ballotlemelo  31745  ballotleme  31754  bnj1152  32270  bnj1280  32292  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem1  32438  ispconn  32470  issconn  32473  cvmsiota  32524  cvmlift2lem12  32561  fmla1  32634  gonan0  32639  goaln0  32640  gonar  32642  goalr  32644  sategoelfvb  32666  rdgprc0  33038  elwlim  33110  neibastop1  33707  neibastop2lem  33708  neibastop2  33709  topdifinffinlem  34631  pibp19  34698  pibp21  34699  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  isprrngo  35343  rabeqel  35531  toycom  36124  isopos  36331  isoml  36389  isatl  36450  iscvlat  36474  ishlat1  36503  cdlemm10N  38269  dihglblem2N  38445  lcfl1lem  38642  lcfls1lem  38685  mapdordlem1a  38785  mapdordlem1  38787  pellqrex  39496  islnm  39697  pwssplit4  39709  islnr  39731  fnlimcnv  41968  stoweidlem14  42319  stoweidlem16  42321  stoweidlem37  42342  stoweidlem48  42353  stoweidlem51  42356  stoweidlem59  42364  salexct  42637  salexct2  42642  salexct3  42645  salgencntex  42646  salgensscntex  42647  ovn0lem  42867  opnvonmbllem1  42934  ovolval5lem2  42955  pimincfltioc  43014  pimdecfgtioo  43015  pimincfltioo  43016  smfresal  43083  smfmullem2  43087  smfpimbor1lem1  43093  smfpimbor1lem2  43094  smfinflem  43111  sprsymrelfo  43679  prproropf1olem1  43685  pairreueq  43692  iseven  43813  isodd  43814  m1expevenALTV  43832  iseven2  43836  isodd3  43837  odd2np1ALTV  43859  opoeALTV  43868  opeoALTV  43869  isgbe  43936  isgbow  43937  isgbo  43938  0nodd  44097  1odd  44098  2nodd  44099  iscmgmALT  44151  issgrpALT  44152  iscsgrpALT  44153  isrng  44167  1neven  44223  2zlidl  44225  2zrngamgm  44230  2zrngagrp  44234  2zrngmmgm  44237  2zrngnmrid  44241  itsclc0  44778  itsclc0b  44779