Theorem elrab2 3663

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465

This theorem is referenced by:  rru  3751  elrabsf  3798  fvmpti  6986  fvmptss2  7014  tfis  7847  elom  7861  oawordeulem  8535  oeeulem  8583  mapfienlem1  9361  mapfienlem3  9363  mapfien  9364  ordtypelem2  9477  ordtypelem3  9478  ordtypelem9  9484  wemapso2lem  9510  inf3lema  9589  oemapvali  9649  tz9.12lem3  9757  cofsmo  10249  enfin2i  10301  fin23lem28  10320  isf32lem6  10338  hsmexlem4  10409  zorn2lem2  10477  pwfseqlem1  10639  pwfseqlem3  10641  nqereu  10910  elz  12589  zsupss  12957  rpnnen1lem5  13001  elrp  13014  repos  13469  wwlktovf  14989  wwlktovf1  14990  wwlktovfo  14991  01sqrexlem1  15289  01sqrexlem2  15290  01sqrexlem6  15294  01sqrexlem7  15295  ello1  15562  elo1  15573  rlimrege0  15626  divalglem2  16449  divalglem4  16450  divalglem5  16451  divalglem9  16455  divalglem10  16456  bitsfzolem  16488  gcdcllem1  16553  gcdcllem2  16554  gcdcllem3  16555  bezoutlem1  16593  bezoutlem3  16595  bezoutlem4  16596  isprm  16727  maxprmfct  16764  phimullem  16834  eulerthlem1  16836  eulerthlem2  16837  hashgcdlem  16843  pclem  16894  pcprecl  16895  pcprendvds  16896  infpn2  16969  prmreclem1  16972  prmreclem2  16973  prmreclem3  16974  prmreclem5  16976  1arith  16983  elgz  16987  4sqlem13  17013  4sqlem17  17017  4sqlem18  17018  vdwnnlem2  17052  vdwnnlem3  17053  ramtlecl  17056  isdrs  18353  istos  18468  islat  18485  isclat  18552  isdlat  18574  istsr  18635  ischn  18659  issgrp  18774  ismnddef  18790  gsumvallem2  18889  isgrp  19002  elnmz  19225  gastacl  19375  gastacos  19376  symgfixelq  19499  psgneldm  19569  sylow1lem2  19665  sylow1lem4  19667  sylow2alem1  19683  sylow2alem2  19684  efgsdm  19796  iscmn  19855  iscyg  19945  iscyggen  19946  dprdw  20078  ablfacrplem  20133  ablfacrp  20134  ablfac1c  20139  ablfac1eu  20141  pgpfaclem1  20149  ablfaclem3  20155  ablfac2  20157  issimpg  20160  isomnd  20189  isrng  20228  issrg  20266  isring  20315  iscrng  20318  isnzr  20593  islring  20621  isrrg  20779  isdomn  20786  isdrng  20813  isorng  20938  islmod  20959  islvec  21199  lspsolvlem  21240  lbsextlem1  21256  lbsextlem3  21258  lbsextlem4  21259  ssdifidllem  21449  ssdifidlprm  21451  islpir  21461  isphl  21743  pjdm  21822  ishil  21833  frlmssuvc1  21909  frlmssuvc2  21910  frlmsslsp  21911  isassa  21971  psrbag  22032  psrbaglefi  22041  psrbagconcl  22042  psrbagleadd1  22043  gsumbagdiaglem  22046  mplelbas  22105  gsummatr01lem1  22777  gsummatr01lem4  22780  gsummatr01  22781  mretopd  23214  neipeltop  23251  isperf  23273  ist0  23442  ist1  23443  ishaus  23444  iscnrm  23445  isreg  23454  isnrm  23457  ispnrm  23461  iscmp  23510  hauscmplem  23528  isconn  23535  conncompss  23555  is1stc  23563  islly  23590  isnlly  23591  dfac14lem  23739  ishmeo  23881  ptcmplem3  24176  ptcmplem4  24177  istmd  24196  istgp  24199  tgpconncompeqg  24234  tgpt0  24241  qustgpopn  24242  istrg  24286  istdrg  24288  istlm  24307  istvc  24314  iscusp  24420  imasdsf1olem  24495  isxms  24569  isms  24571  blcld  24627  prdsxmslem2  24651  isngp  24718  isnrg  24782  isnlm  24797  icccmplem1  24945  icccmplem2  24946  isclm  25188  iscph  25294  isbn  25462  iscms  25469  ivthlem1  25575  ivthlem2  25576  ivthlem3  25577  elovolm  25599  ovolicc2lem2  25642  ovolicc2lem4  25644  ovolicc2lem5  25645  ismbl  25650  dyadmbllem  25723  dyadmbl  25724  ismbf1  25748  isi1f  25798  isibl  25889  isuc1p  26263  ismon1p  26265  radcnvle  26545  abelthlem2  26557  abelthlem7a  26562  atans  27057  lgamgulmlem2  27156  lgamgulmlem3  27157  lgamgulmlem5  27159  lgambdd  27163  wilthlem2  27195  wilthlem3  27196  ftalem3  27201  sqff1o  27308  mpodvdsmulf1o  27320  dvdsmulf1o  27322  lgslem2  27424  lgslem3  27425  lgsfcl2  27429  rpvmasumlem  27613  dchrvmaeq0  27630  dchrisum0re  27639  pntlem3  27735  elleft  28006  elright  28007  elons  28408  elreno  28646  axcontlem2  29252  lfgredgge2  29411  uspgredg2vlem  29510  uspgredg2v  29511  usgredg2vlem1  29512  usgredg2vlem2  29513  ushgredgedg  29516  ushgredgedgloop  29518  uhgrspan1  29590  upgrreslem  29591  umgrreslem  29592  isfusgr  29605  nbupgrres  29651  nbusgredgeu0  29655  nbusgrf1o0  29656  uvtxel  29675  uvtxel1  29683  cusgrexilem2  29729  cusgrfilem2  29743  vtxdginducedm1lem4  29829  rgrx0ndm  29880  iswspthn  30135  wwlknon  30143  wspthnon  30144  wwlksn0  30149  wwlksnextfun  30184  wwlksnextinj  30185  wwlksnextsurj  30186  wwlksnextproplem3  30197  clwlkclwwlkflem  30292  clwlkclwwlkfolem  30295  isclwwlkn  30315  clwwlkel  30334  clwwlkf  30335  clwwlkf1  30337  isclwwlknon  30379  s2elclwwlknon2  30392  isfrgr  30548  frgrwopreglem3  30602  frgrwopreglem5lem  30608  frgrwopreglem5  30609  isablo  30835  iscbn  31153  hcau  31473  issh  31497  isch  31511  elcnop  32146  ellnop  32147  elbdop  32149  elhmop  32162  elcnfn  32171  ellnfn  32172  isst  32502  ishst  32503  ela  32628  isslmd  33459  elrgspnlem1  33499  elrgspnlem2  33500  elrgspnlem4  33502  elrgspn  33503  ssmxidllem  33697  isufd  33771  iscref  34175  isrrext  34331  ispisys  34483  isldsys  34487  isros  34499  issros  34506  oddpwdc  34685  eulerpartleme  34694  eulerpartlemo  34696  eulerpartlemd  34697  eulerpartlemt0  34700  eulerpartlemf  34701  eulerpartlemt  34702  eulerpartlemr  34705  eulerpartlemmf  34706  eulerpartlemgvv  34707  eulerpartlemgs2  34711  eulerpartlemn  34712  elprob  34740  ballotlemelo  34819  ballotleme  34828  bnj1152  35327  bnj1280  35349  subfacp1lem3  35569  subfacp1lem5  35571  erdszelem1  35578  ispconn  35610  issconn  35613  cvmsiota  35664  cvmlift2lem12  35701  fmla1  35774  gonan0  35779  goaln0  35780  gonar  35782  goalr  35784  sategoelfvb  35806  rdgprc0  36178  elwlim  36208  neibastop1  36755  neibastop2lem  36756  neibastop2  36757  topdifinffinlem  37876  pibp19  37943  pibp21  37944  poimirlem5  38159  poimirlem6  38160  poimirlem7  38161  poimirlem8  38162  poimirlem10  38164  poimirlem11  38165  poimirlem12  38166  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem18  38172  poimirlem19  38173  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  isprrngo  38584  rabeqel  38791  toycom  39632  isopos  39839  isoml  39897  isatl  39958  iscvlat  39982  ishlat1  40011  cdlemm10N  41777  dihglblem2N  41953  lcfl1lem  42150  lcfls1lem  42193  mapdordlem1a  42293  mapdordlem1  42295  iscsrg  42623  readvcot  43010  mhphflem  43215  pellqrex  43493  islnm  43691  pwssplit4  43703  islnr  43725  fnlimcnv  46268  stoweidlem14  46615  stoweidlem16  46617  stoweidlem37  46638  stoweidlem48  46649  stoweidlem51  46652  stoweidlem59  46660  salexct  46935  salexct2  46940  salexct3  46943  salgencntex  46944  salgensscntex  46945  ovn0lem  47166  opnvonmbllem1  47233  ovolval5lem2  47254  pimincfltioc  47317  pimdecfgtioo  47318  pimincfltioo  47319  smfresal  47389  smfmullem2  47393  smfpimbor1lem1  47399  smfpimbor1lem2  47400  smfinflem  47418  sprsymrelfo  48130  prproropf1olem1  48136  pairreueq  48143  iseven  48277  isodd  48278  m1expevenALTV  48296  iseven2  48300  isodd3  48301  odd2np1ALTV  48323  opoeALTV  48332  opeoALTV  48333  isgbe  48400  isgbow  48401  isgbo  48402  uspgrlimlem2  48638  uspgrlimlem3  48639  uspgrlimlem4  48640  clnbgrvtxedg  48643  grlimpredg  48647  grlimprclnbgrvtx  48648  grlimgrtrilem1  48650  0nodd  48819  1odd  48820  2nodd  48821  iscmgmALT  48873  issgrpALT  48874  iscsgrpALT  48875  1neven  48887  2zlidl  48889  2zrngamgm  48894  2zrngagrp  48898  2zrngmmgm  48901  2zrngnmrid  48905  isprmrng  48985  itsclc0  49431  itsclc0b  49432  isthinc  50077  istermc  50132