Theorem elrab2 3685

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

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

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498

This theorem is referenced by:  rru  3772  elrabsf  3818  fvmpti  6769  fvmptss2  6795  tfis  7571  elom  7585  oawordeulem  8182  oeeulem  8229  mapfienlem1  8870  mapfienlem3  8872  mapfien  8873  ordtypelem2  8985  ordtypelem3  8986  ordtypelem9  8992  wemapso2lem  9018  inf3lema  9089  oemapvali  9149  tz9.12lem3  9220  cofsmo  9693  enfin2i  9745  fin23lem28  9764  isf32lem6  9782  hsmexlem4  9853  zorn2lem2  9921  pwfseqlem1  10082  pwfseqlem3  10084  nqereu  10353  elz  11986  zsupss  12340  rpnnen1lem5  12383  elrp  12394  repos  12837  wwlktovf  14322  wwlktovf1  14323  wwlktovfo  14324  sqrlem1  14604  sqrlem2  14605  sqrlem6  14609  sqrlem7  14610  ello1  14874  elo1  14885  rlimrege0  14938  divalglem2  15748  divalglem4  15749  divalglem5  15750  divalglem9  15754  divalglem10  15755  bitsfzolem  15785  gcdcllem1  15850  gcdcllem2  15851  gcdcllem3  15852  bezoutlem1  15889  bezoutlem3  15891  bezoutlem4  15892  isprm  16019  maxprmfct  16055  phimullem  16118  eulerthlem1  16120  eulerthlem2  16121  hashgcdlem  16127  pclem  16177  pcprecl  16178  pcprendvds  16179  infpn2  16251  prmreclem1  16254  prmreclem2  16255  prmreclem3  16256  prmreclem5  16258  1arith  16265  elgz  16269  4sqlem13  16295  4sqlem17  16299  4sqlem18  16300  vdwnnlem2  16334  vdwnnlem3  16335  ramtlecl  16338  isdrs  17546  istos  17647  islat  17659  isclat  17721  isdlat  17805  istsr  17829  issgrp  17904  ismnddef  17915  gsumvallem2  18000  isgrp  18111  elnmz  18317  gastacl  18441  gastacos  18442  symgfixelq  18563  psgneldm  18633  sylow1lem2  18726  sylow1lem4  18728  sylow2alem1  18744  sylow2alem2  18745  efgsdm  18858  iscmn  18916  iscyg  19000  iscyggen  19001  dprdw  19134  ablfacrplem  19189  ablfacrp  19190  ablfac1c  19195  ablfac1eu  19197  pgpfaclem1  19205  ablfaclem3  19211  ablfac2  19213  issimpg  19216  issrg  19259  isring  19303  iscrng  19306  isdrng  19508  islmod  19640  islvec  19878  lspsolvlem  19916  lbsextlem1  19932  lbsextlem3  19934  lbsextlem4  19935  islpir  20024  isnzr  20034  isrrg  20063  isdomn  20069  isassa  20090  psrbag  20146  psrbaglefi  20154  psrbagconcl  20155  psrbagconf1o  20156  gsumbagdiaglem  20157  mplelbas  20212  isphl  20774  pjdm  20853  ishil  20864  frlmssuvc1  20940  frlmssuvc2  20941  frlmsslsp  20942  gsummatr01lem1  21266  gsummatr01lem4  21269  gsummatr01  21270  mretopd  21702  neipeltop  21739  isperf  21761  ist0  21930  ist1  21931  ishaus  21932  iscnrm  21933  isreg  21942  isnrm  21945  ispnrm  21949  iscmp  21998  hauscmplem  22016  isconn  22023  conncompss  22043  is1stc  22051  islly  22078  isnlly  22079  dfac14lem  22227  ishmeo  22369  ptcmplem3  22664  ptcmplem4  22665  istmd  22684  istgp  22687  tgpconncompeqg  22722  tgpt0  22729  qustgpopn  22730  istrg  22774  istdrg  22776  istlm  22795  istvc  22802  iscusp  22910  imasdsf1olem  22985  isxms  23059  isms  23061  blcld  23117  prdsxmslem2  23141  isngp  23207  isnrg  23271  isnlm  23286  icccmplem1  23432  icccmplem2  23433  isclm  23670  iscph  23776  isbn  23943  iscms  23950  ivthlem1  24054  ivthlem2  24055  ivthlem3  24056  elovolm  24078  ovolicc2lem2  24121  ovolicc2lem4  24123  ovolicc2lem5  24124  ismbl  24129  dyadmbllem  24202  dyadmbl  24203  ismbf1  24227  isi1f  24277  isibl  24368  isuc1p  24736  ismon1p  24738  radcnvle  25010  abelthlem2  25022  abelthlem7a  25027  atans  25510  lgamgulmlem2  25609  lgamgulmlem3  25610  lgamgulmlem5  25612  lgambdd  25616  wilthlem2  25648  wilthlem3  25649  ftalem3  25654  sqff1o  25761  dvdsmulf1o  25773  lgslem2  25876  lgslem3  25877  lgsfcl2  25881  rpvmasumlem  26065  dchrvmaeq0  26082  dchrisum0re  26091  pntlem3  26187  axcontlem2  26753  lfgredgge2  26911  uspgredg2vlem  27007  uspgredg2v  27008  usgredg2vlem1  27009  usgredg2vlem2  27010  ushgredgedg  27013  ushgredgedgloop  27015  uhgrspan1  27087  upgrreslem  27088  umgrreslem  27089  isfusgr  27102  nbupgrres  27148  nbusgredgeu0  27152  nbusgrf1o0  27153  uvtxel  27172  uvtxel1  27180  cusgrexilem2  27226  cusgrfilem2  27240  vtxdginducedm1lem4  27326  rgrx0ndm  27377  iswspthn  27629  wwlknon  27637  wspthnon  27638  wwlksn0  27643  wwlksnextfun  27678  wwlksnextinj  27679  wwlksnextsurj  27680  wwlksnextproplem3  27692  clwlkclwwlkflem  27784  clwlkclwwlkfolem  27787  isclwwlkn  27807  clwwlkel  27827  clwwlkf  27828  clwwlkf1  27830  isclwwlknon  27872  s2elclwwlknon2  27885  isfrgr  28041  frgrwopreglem3  28095  frgrwopreglem5lem  28101  frgrwopreglem5  28102  isablo  28325  iscbn  28643  hcau  28963  issh  28987  isch  29001  elcnop  29636  ellnop  29637  elbdop  29639  elhmop  29652  elcnfn  29661  ellnfn  29662  isst  29992  ishst  29993  ela  30118  isomnd  30704  isslmd  30832  isorng  30874  ssmxidllem  30980  iscref  31110  isrrext  31243  ispisys  31413  isldsys  31417  isros  31429  issros  31436  oddpwdc  31614  eulerpartleme  31623  eulerpartlemo  31625  eulerpartlemd  31626  eulerpartlemt0  31629  eulerpartlemf  31630  eulerpartlemt  31631  eulerpartlemr  31634  eulerpartlemmf  31635  eulerpartlemgvv  31636  eulerpartlemgs2  31640  eulerpartlemn  31641  elprob  31669  ballotlemelo  31747  ballotleme  31756  bnj1152  32272  bnj1280  32294  subfacp1lem3  32431  subfacp1lem5  32433  erdszelem1  32440  ispconn  32472  issconn  32475  cvmsiota  32526  cvmlift2lem12  32563  fmla1  32636  gonan0  32641  goaln0  32642  gonar  32644  goalr  32646  sategoelfvb  32668  rdgprc0  33040  elwlim  33112  neibastop1  33709  neibastop2lem  33710  neibastop2  33711  topdifinffinlem  34630  pibp19  34697  pibp21  34698  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  isprrngo  35330  rabeqel  35518  toycom  36111  isopos  36318  isoml  36376  isatl  36437  iscvlat  36461  ishlat1  36490  cdlemm10N  38256  dihglblem2N  38432  lcfl1lem  38629  lcfls1lem  38672  mapdordlem1a  38772  mapdordlem1  38774  pellqrex  39483  islnm  39684  pwssplit4  39696  islnr  39718  fnlimcnv  41955  stoweidlem14  42306  stoweidlem16  42308  stoweidlem37  42329  stoweidlem48  42340  stoweidlem51  42343  stoweidlem59  42351  salexct  42624  salexct2  42629  salexct3  42632  salgencntex  42633  salgensscntex  42634  ovn0lem  42854  opnvonmbllem1  42921  ovolval5lem2  42942  pimincfltioc  43001  pimdecfgtioo  43002  pimincfltioo  43003  smfresal  43070  smfmullem2  43074  smfpimbor1lem1  43080  smfpimbor1lem2  43081  smfinflem  43098  sprsymrelfo  43666  prproropf1olem1  43672  pairreueq  43679  iseven  43800  isodd  43801  m1expevenALTV  43819  iseven2  43823  isodd3  43824  odd2np1ALTV  43846  opoeALTV  43855  opeoALTV  43856  isgbe  43923  isgbow  43924  isgbo  43925  0nodd  44084  1odd  44085  2nodd  44086  iscmgmALT  44138  issgrpALT  44139  iscsgrpALT  44140  isrng  44154  1neven  44210  2zlidl  44212  2zrngamgm  44217  2zrngagrp  44221  2zrngmmgm  44224  2zrngnmrid  44228  itsclc0  44765  itsclc0b  44766