Theorem elrab2 3652

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455

This theorem is referenced by:  rru  3740  elrabsf  3787  fvmpti  6969  fvmptss2  6997  tfis  7830  elom  7844  oawordeulem  8517  oeeulem  8565  mapfienlem1  9345  mapfienlem3  9347  mapfien  9348  ordtypelem2  9461  ordtypelem3  9462  ordtypelem9  9468  wemapso2lem  9494  inf3lema  9573  oemapvali  9633  tz9.12lem3  9741  cofsmo  10220  enfin2i  10272  fin23lem28  10291  isf32lem6  10309  hsmexlem4  10380  zorn2lem2  10448  pwfseqlem1  10610  pwfseqlem3  10612  nqereu  10881  elz  12564  zsupss  12932  rpnnen1lem5  12976  elrp  12989  repos  13444  wwlktovf  14963  wwlktovf1  14964  wwlktovfo  14965  01sqrexlem1  15260  01sqrexlem2  15261  01sqrexlem6  15265  01sqrexlem7  15266  ello1  15533  elo1  15544  rlimrege0  15597  divalglem2  16420  divalglem4  16421  divalglem5  16422  divalglem9  16426  divalglem10  16427  bitsfzolem  16459  gcdcllem1  16524  gcdcllem2  16525  gcdcllem3  16526  bezoutlem1  16564  bezoutlem3  16566  bezoutlem4  16567  isprm  16698  maxprmfct  16735  phimullem  16805  eulerthlem1  16807  eulerthlem2  16808  hashgcdlem  16814  pclem  16865  pcprecl  16866  pcprendvds  16867  infpn2  16940  prmreclem1  16943  prmreclem2  16944  prmreclem3  16945  prmreclem5  16947  1arith  16954  elgz  16958  4sqlem13  16984  4sqlem17  16988  4sqlem18  16989  vdwnnlem2  17023  vdwnnlem3  17024  ramtlecl  17027  isdrs  18324  istos  18439  islat  18456  isclat  18523  isdlat  18545  istsr  18606  ischn  18630  issgrp  18745  ismnddef  18761  gsumvallem2  18859  isgrp  18972  elnmz  19195  gastacl  19340  gastacos  19341  symgfixelq  19464  psgneldm  19534  sylow1lem2  19630  sylow1lem4  19632  sylow2alem1  19648  sylow2alem2  19649  efgsdm  19761  iscmn  19820  iscyg  19910  iscyggen  19911  dprdw  20043  ablfacrplem  20098  ablfacrp  20099  ablfac1c  20104  ablfac1eu  20106  pgpfaclem1  20114  ablfaclem3  20120  ablfac2  20122  issimpg  20125  isomnd  20154  isrng  20191  issrg  20225  isring  20274  iscrng  20277  isnzr  20551  islring  20577  isrrg  20735  isdomn  20742  isdrng  20770  isorng  20898  islmod  20919  islvec  21159  lspsolvlem  21200  lbsextlem1  21216  lbsextlem3  21218  lbsextlem4  21219  islpir  21386  isphl  21668  pjdm  21747  ishil  21758  frlmssuvc1  21834  frlmssuvc2  21835  frlmsslsp  21836  isassa  21896  psrbag  21957  psrbaglefi  21966  psrbagconcl  21967  psrbagleadd1  21968  gsumbagdiaglem  21971  mplelbas  22030  gsummatr01lem1  22703  gsummatr01lem4  22706  gsummatr01  22707  mretopd  23140  neipeltop  23177  isperf  23199  ist0  23368  ist1  23369  ishaus  23370  iscnrm  23371  isreg  23380  isnrm  23383  ispnrm  23387  iscmp  23436  hauscmplem  23454  isconn  23461  conncompss  23481  is1stc  23489  islly  23516  isnlly  23517  dfac14lem  23665  ishmeo  23807  ptcmplem3  24102  ptcmplem4  24103  istmd  24122  istgp  24125  tgpconncompeqg  24160  tgpt0  24167  qustgpopn  24168  istrg  24212  istdrg  24214  istlm  24233  istvc  24240  iscusp  24346  imasdsf1olem  24421  isxms  24495  isms  24497  blcld  24553  prdsxmslem2  24577  isngp  24644  isnrg  24708  isnlm  24723  icccmplem1  24871  icccmplem2  24872  isclm  25114  iscph  25220  isbn  25388  iscms  25395  ivthlem1  25501  ivthlem2  25502  ivthlem3  25503  elovolm  25525  ovolicc2lem2  25568  ovolicc2lem4  25570  ovolicc2lem5  25571  ismbl  25576  dyadmbllem  25649  dyadmbl  25650  ismbf1  25674  isi1f  25724  isibl  25815  isuc1p  26189  ismon1p  26191  radcnvle  26471  abelthlem2  26483  abelthlem7a  26488  atans  26983  lgamgulmlem2  27082  lgamgulmlem3  27083  lgamgulmlem5  27085  lgambdd  27089  wilthlem2  27121  wilthlem3  27122  ftalem3  27127  sqff1o  27234  mpodvdsmulf1o  27246  dvdsmulf1o  27248  lgslem2  27350  lgslem3  27351  lgsfcl2  27355  rpvmasumlem  27539  dchrvmaeq0  27556  dchrisum0re  27565  pntlem3  27661  elleft  27932  elright  27933  elons  28334  elreno  28572  axcontlem2  29123  lfgredgge2  29282  uspgredg2vlem  29381  uspgredg2v  29382  usgredg2vlem1  29383  usgredg2vlem2  29384  ushgredgedg  29387  ushgredgedgloop  29389  uhgrspan1  29461  upgrreslem  29462  umgrreslem  29463  isfusgr  29476  nbupgrres  29522  nbusgredgeu0  29526  nbusgrf1o0  29527  uvtxel  29546  uvtxel1  29554  cusgrexilem2  29600  cusgrfilem2  29614  vtxdginducedm1lem4  29700  rgrx0ndm  29751  iswspthn  30006  wwlknon  30014  wspthnon  30015  wwlksn0  30020  wwlksnextfun  30055  wwlksnextinj  30056  wwlksnextsurj  30057  wwlksnextproplem3  30068  clwlkclwwlkflem  30163  clwlkclwwlkfolem  30166  isclwwlkn  30186  clwwlkel  30205  clwwlkf  30206  clwwlkf1  30208  isclwwlknon  30250  s2elclwwlknon2  30263  isfrgr  30419  frgrwopreglem3  30473  frgrwopreglem5lem  30479  frgrwopreglem5  30480  isablo  30706  iscbn  31024  hcau  31344  issh  31368  isch  31382  elcnop  32017  ellnop  32018  elbdop  32020  elhmop  32033  elcnfn  32042  ellnfn  32043  isst  32373  ishst  32374  ela  32499  isslmd  33343  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem4  33387  elrgspn  33388  ssdifidllem  33604  ssdifidlprm  33606  ssmxidllem  33622  isufd  33697  iscref  34102  isrrext  34258  ispisys  34410  isldsys  34414  isros  34426  issros  34433  oddpwdc  34612  eulerpartleme  34621  eulerpartlemo  34623  eulerpartlemd  34624  eulerpartlemt0  34627  eulerpartlemf  34628  eulerpartlemt  34629  eulerpartlemr  34632  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgs2  34638  eulerpartlemn  34639  elprob  34667  ballotlemelo  34746  ballotleme  34755  bnj1152  35254  bnj1280  35276  subfacp1lem3  35493  subfacp1lem5  35495  erdszelem1  35502  ispconn  35534  issconn  35537  cvmsiota  35588  cvmlift2lem12  35625  fmla1  35698  gonan0  35703  goaln0  35704  gonar  35706  goalr  35708  sategoelfvb  35730  rdgprc0  36102  elwlim  36132  neibastop1  36680  neibastop2lem  36681  neibastop2  36682  topdifinffinlem  37802  pibp19  37869  pibp21  37870  poimirlem5  38085  poimirlem6  38086  poimirlem7  38087  poimirlem8  38088  poimirlem10  38090  poimirlem11  38091  poimirlem12  38092  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem18  38098  poimirlem19  38099  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  isprrngo  38510  rabeqel  38717  toycom  39558  isopos  39765  isoml  39823  isatl  39884  iscvlat  39908  ishlat1  39937  cdlemm10N  41703  dihglblem2N  41879  lcfl1lem  42076  lcfls1lem  42119  mapdordlem1a  42219  mapdordlem1  42221  iscsrg  42549  readvcot  42934  mhphflem  43139  pellqrex  43417  islnm  43615  pwssplit4  43627  islnr  43649  fnlimcnv  46202  stoweidlem14  46549  stoweidlem16  46551  stoweidlem37  46572  stoweidlem48  46583  stoweidlem51  46586  stoweidlem59  46594  salexct  46869  salexct2  46874  salexct3  46877  salgencntex  46878  salgensscntex  46879  ovn0lem  47100  opnvonmbllem1  47167  ovolval5lem2  47188  pimincfltioc  47251  pimdecfgtioo  47252  pimincfltioo  47253  smfresal  47323  smfmullem2  47327  smfpimbor1lem1  47333  smfpimbor1lem2  47334  smfinflem  47352  sprsymrelfo  48064  prproropf1olem1  48070  pairreueq  48077  iseven  48211  isodd  48212  m1expevenALTV  48230  iseven2  48234  isodd3  48235  odd2np1ALTV  48257  opoeALTV  48266  opeoALTV  48267  isgbe  48334  isgbow  48335  isgbo  48336  uspgrlimlem2  48572  uspgrlimlem3  48573  uspgrlimlem4  48574  clnbgrvtxedg  48577  grlimpredg  48581  grlimprclnbgrvtx  48582  grlimgrtrilem1  48584  0nodd  48753  1odd  48754  2nodd  48755  iscmgmALT  48807  issgrpALT  48808  iscsgrpALT  48809  1neven  48821  2zlidl  48823  2zrngamgm  48828  2zrngagrp  48832  2zrngmmgm  48835  2zrngnmrid  48839  itsclc0  49354  itsclc0b  49355  isthinc  50001  istermc  50056