Theorem elrab2 3333

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175

This theorem is referenced by:  elrabsf  3441  pwnss  4756  fvmpti  6190  fvmptss2  6212  tfis  6946  elom  6960  oawordeulem  7521  oeeulem  7568  mapfienlem1  8193  mapfienlem3  8195  mapfien  8196  ordtypelem2  8307  ordtypelem3  8308  ordtypelem9  8314  wemapso2lem  8340  inf3lema  8404  oemapvali  8464  tz9.12lem3  8535  cofsmo  8974  enfin2i  9026  fin23lem28  9045  isf32lem6  9063  hsmexlem4  9134  zorn2lem2  9202  pwfseqlem1  9359  pwfseqlem3  9361  nqereu  9630  elz  11256  zsupss  11653  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  elrp  11710  repos  12141  wwlktovf  13547  wwlktovf1  13548  wwlktovfo  13549  sqrlem1  13831  sqrlem2  13832  sqrlem6  13836  sqrlem7  13837  ello1  14094  elo1  14105  rlimrege0  14158  divalglem2  14956  divalglem4  14957  divalglem5  14958  divalglem9  14962  divalglem10  14963  bitsfzolem  14994  gcdcllem1  15059  gcdcllem2  15060  gcdcllem3  15061  bezoutlem1  15094  bezoutlem3  15096  bezoutlem4  15097  isprm  15225  maxprmfct  15259  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  hashgcdlem  15331  pclem  15381  pcprecl  15382  pcprendvds  15383  infpn2  15455  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  1arith  15469  elgz  15473  4sqlem13  15499  4sqlem17  15503  4sqlem18  15504  vdwnnlem2  15538  vdwnnlem3  15539  ramtlecl  15542  isdrs  16757  istos  16858  islat  16870  isclat  16932  isdlat  17016  istsr  17040  issgrp  17108  ismnddef  17119  gsumvallem2  17195  isgrp  17251  elnmz  17456  gastacl  17565  gastacos  17566  symgfixelq  17676  psgneldm  17746  sylow1lem2  17837  sylow1lem4  17839  sylow2alem1  17855  sylow2alem2  17856  efgsdm  17966  iscmn  18023  iscyg  18104  iscyggen  18105  dprdw  18232  ablfacrplem  18287  ablfacrp  18288  ablfac1c  18293  ablfac1eu  18295  pgpfaclem1  18303  ablfaclem3  18309  ablfac2  18311  issrg  18330  isring  18374  iscrng  18377  isdrng  18574  islmod  18690  islvec  18925  lspsolvlem  18963  lbsextlem1  18979  lbsextlem3  18981  lbsextlem4  18982  islpir  19070  isnzr  19080  isrrg  19109  isdomn  19115  isassa  19136  psrbag  19185  psrbaglefi  19193  psrbagconcl  19194  psrbagconf1o  19195  gsumbagdiaglem  19196  mplelbas  19251  isphl  19792  pjdm  19870  ishil  19881  frlmssuvc1  19952  frlmssuvc2  19953  frlmsslsp  19954  gsummatr01lem1  20280  gsummatr01lem4  20283  gsummatr01  20284  mretopd  20706  neipeltop  20743  isperf  20765  ist0  20934  ist1  20935  ishaus  20936  iscnrm  20937  isreg  20946  isnrm  20949  ispnrm  20953  iscmp  21001  hauscmplem  21019  iscon  21026  concompss  21046  is1stc  21054  islly  21081  isnlly  21082  dfac14lem  21230  ishmeo  21372  ptcmplem3  21668  ptcmplem4  21669  istmd  21688  istgp  21691  tgpconcompeqg  21725  tgpt0  21732  qustgpopn  21733  istrg  21777  istdrg  21779  istlm  21798  istvc  21805  iscusp  21913  imasdsf1olem  21988  isxms  22062  isms  22064  blcld  22120  prdsxmslem2  22144  isngp  22210  isnrg  22274  isnlm  22289  icccmplem1  22433  icccmplem2  22434  isclm  22672  iscph  22778  isbn  22943  iscms  22950  ivthlem1  23027  ivthlem2  23028  ivthlem3  23029  elovolm  23050  ovolicc2lem2  23093  ovolicc2lem4  23095  ovolicc2lem5  23096  ismbl  23101  dyadmbllem  23173  dyadmbl  23174  ismbf1  23199  isi1f  23247  isibl  23338  isuc1p  23704  ismon1p  23706  radcnvle  23978  abelthlem2  23990  abelthlem7a  23995  atans  24457  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  wilthlem2  24595  wilthlem3  24596  ftalem3  24601  sqff1o  24708  dvdsmulf1o  24720  lgslem2  24823  lgslem3  24824  lgsfcl2  24828  rpvmasumlem  24976  dchrvmaeq0  24993  dchrisum0re  25002  pntlem3  25098  axcontlem2  25645  lfgredgge2  25790  usgraidx2vlem1  25920  usgraidx2vlem2  25921  cusgraexi  25997  cusgrafilem2  26008  wlknwwlknfun  26238  wlknwwlkninj  26239  wlkiswwlkfun  26245  wlkiswwlkinj  26246  wlkiswwlksur  26247  wwlkextfun  26257  wwlkextinj  26258  wwlkextsur  26259  wwlkextproplem3  26271  clwwlkel  26321  clwwlkf  26322  clwwlkf1  26324  clwlkfclwwlk1hashn  26368  clwlkfoclwwlk  26372  clwlkf1clwwlklem1  26373  clwlkf1clwwlklem2  26374  clwlkf1clwwlklem3  26375  frgrawopreglem3  26573  extwwlkfab  26617  isablo  26784  iscbn  27104  hcau  27425  issh  27449  isch  27463  elcnop  28100  ellnop  28101  elbdop  28103  elhmop  28116  elcnfn  28125  ellnfn  28126  isst  28456  ishst  28457  ela  28582  isomnd  29032  isslmd  29086  isorng  29130  iscref  29239  isrrext  29372  ispisys  29542  isldsys  29546  isros  29558  issros  29565  oddpwdc  29743  eulerpartleme  29752  eulerpartlemo  29754  eulerpartlemd  29755  eulerpartlemt0  29758  eulerpartlemf  29759  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgs2  29769  eulerpartlemn  29770  elprob  29798  ballotlemelo  29876  ballotleme  29885  bnj1152  30320  bnj1280  30342  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem1  30427  ispcon  30459  isscon  30462  cvmsiota  30513  cvmlift2lem12  30550  rdgprc0  30943  elwlim  31013  elwlimOLD  31014  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  topdifinffinlem  32371  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  isprrngo  33019  toycom  33278  isopos  33485  isoml  33543  isatl  33604  iscvlat  33628  ishlat1  33657  cdlemm10N  35425  dihglblem2N  35601  lcfl1lem  35798  lcfls1lem  35841  mapdordlem1a  35941  mapdordlem1  35943  pellqrex  36461  islnm  36665  pwssplit4  36677  islnr  36700  fnlimcnv  38734  stoweidlem14  38907  stoweidlem16  38909  stoweidlem37  38930  stoweidlem48  38941  stoweidlem51  38944  stoweidlem59  38952  salexct  39228  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  ovn0lem  39455  opnvonmbllem1  39522  ovolval5lem2  39543  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  smfresal  39673  smfmullem2  39677  smfpimbor1lem1  39683  smfpimbor1lem2  39684  m1expevenALTV  40098  iseven2  40102  isodd3  40103  odd2np1ALTV  40123  opoeALTV  40132  opeoALTV  40133  isgbe  40173  isgbo  40174  isgboa  40175  uspgredg2vlem  40450  uspgredg2v  40451  usgredg2vlem1  40452  usgredg2vlem2  40453  ushgredgedga  40456  ushgredgedgaloop  40458  uhgrspan1  40527  isfusgr  40537  nbupgrres  40592  iscusgr  40640  cusgrexi  40662  cusgrfilem2  40672  iswspthn  41047  wlknwwlksnfun  41085  wlknwwlksninj  41086  wlkwwlkfun  41092  wlkwwlkinj  41093  wlkwwlksur  41094  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextsur  41106  wwlksnextproplem3  41117  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  clwlksfclwwlk1hashn  41266  clwlksfoclwwlk  41270  clwlksf1clwwlklem0  41271  frgrwopreglem3  41483  av-extwwlkfab  41520  0nodd  41600  1odd  41601  2nodd  41602  iscmgmALT  41650  issgrpALT  41651  iscsgrpALT  41652  isrng  41666  1neven  41722  2zlidl  41724  2zrngamgm  41729  2zrngagrp  41733  2zrngmmgm  41736  2zrngnmrid  41740