Theorem elrab2 3656

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {crab 3418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459

This theorem is used by:  rru  3744  elrabsf  3791  fvmpti  6992  fvmptss2  7020  tfis  7857  elom  7871  oawordeulem  8545  oeeulem  8593  mapfienlem1  9372  mapfienlem3  9374  mapfien  9375  ordtypelem2  9488  ordtypelem3  9489  ordtypelem9  9495  wemapso2lem  9521  inf3lema  9600  oemapvali  9660  tz9.12lem3  9768  cofsmo  10268  enfin2i  10320  fin23lem28  10339  isf32lem6  10357  hsmexlem4  10428  zorn2lem2  10496  pwfseqlem1  10658  pwfseqlem3  10660  nqereu  10929  elz  12608  zsupss  12977  rpnnen1lem5  13021  elrp  13034  repos  13489  wwlktovf  15017  wwlktovf1  15018  wwlktovfo  15019  01sqrexlem1  15317  01sqrexlem2  15318  01sqrexlem6  15322  01sqrexlem7  15323  ello1  15590  elo1  15601  rlimrege0  15654  divalglem2  16475  divalglem4  16476  divalglem5  16477  divalglem9  16481  divalglem10  16482  bitsfzolem  16514  gcdcllem1  16579  gcdcllem2  16580  gcdcllem3  16581  bezoutlem1  16619  bezoutlem3  16621  bezoutlem4  16622  isprm  16753  maxprmfct  16790  phimullem  16860  eulerthlem1  16862  eulerthlem2  16863  hashgcdlem  16869  pclem  16920  pcprecl  16921  pcprendvds  16922  infpn2  16995  prmreclem1  16998  prmreclem2  16999  prmreclem3  17000  prmreclem5  17002  1arith  17009  elgz  17013  4sqlem13  17039  4sqlem17  17043  4sqlem18  17044  vdwnnlem2  17078  vdwnnlem3  17079  ramtlecl  17082  isdrs  18379  istos  18494  islat  18511  isclat  18578  isdlat  18600  istsr  18661  ischn  18685  issgrp  18810  ismnddef  18826  gsumvallem2  18930  isgrp  19050  elnmz  19273  gastacl  19423  gastacos  19424  symgfixelq  19547  psgneldm  19617  sylow1lem2  19713  sylow1lem4  19715  sylow2alem1  19731  sylow2alem2  19732  efgsdm  19844  iscmn  19903  iscyg  19993  iscyggen  19994  dprdw  20126  ablfacrplem  20181  ablfacrp  20182  ablfac1c  20187  ablfac1eu  20189  pgpfaclem1  20197  ablfaclem3  20203  ablfac2  20205  issimpg  20208  isomnd  20237  isrng  20276  issrg  20314  isring  20363  iscrng  20366  isnzr  20661  islring  20689  isrrg  20847  isdomn  20854  isdrng  20881  isorng  21014  islmod  21035  islvec  21275  lspsolvlem  21316  lbsextlem1  21332  lbsextlem3  21334  lbsextlem4  21335  ssdifidllem  21534  ssdifidlprm  21536  islpir  21546  isphl  21828  pjdm  21907  ishil  21918  frlmssuvc1  21994  frlmssuvc2  21995  frlmsslsp  21996  isassa  22056  psrbag  22117  psrbaglefi  22126  psrbagconcl  22127  psrbagleadd1  22128  gsumbagdiaglem  22131  mplelbas  22190  gsummatr01lem1  22862  gsummatr01lem4  22865  gsummatr01  22866  mretopd  23299  neipeltop  23336  isperf  23358  ist0  23527  ist1  23528  ishaus  23529  iscnrm  23530  isreg  23539  isnrm  23542  ispnrm  23546  iscmp  23595  hauscmplem  23613  isconn  23620  conncompss  23640  is1stc  23648  islly  23676  isnlly  23677  dfac14lem  23825  ishmeo  23967  ptcmplem3  24262  ptcmplem4  24263  istmd  24282  istgp  24285  tgpconncompeqg  24320  tgpt0  24327  qustgpopn  24328  istrg  24372  istdrg  24374  istlm  24393  istvc  24400  iscusp  24506  imasdsf1olem  24581  isxms  24655  isms  24657  blcld  24713  prdsxmslem2  24737  isngp  24804  isnrg  24868  isnlm  24883  icccmplem1  25031  icccmplem2  25032  isclm  25274  iscph  25380  isbn  25548  iscms  25555  ivthlem1  25661  ivthlem2  25662  ivthlem3  25663  elovolm  25685  ovolicc2lem2  25728  ovolicc2lem4  25730  ovolicc2lem5  25731  ismbl  25736  dyadmbllem  25809  dyadmbl  25810  ismbf1  25834  isi1f  25884  isibl  25975  isuc1p  26349  ismon1p  26351  radcnvle  26634  abelthlem2  26646  abelthlem7a  26651  atans  27146  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamgulmlem5  27248  lgambdd  27252  wilthlem2  27284  wilthlem3  27285  ftalem3  27290  sqff1o  27397  mpodvdsmulf1o  27409  dvdsmulf1o  27411  lgslem2  27513  lgslem3  27514  lgsfcl2  27518  rpvmasumlem  27702  dchrvmaeq0  27719  dchrisum0re  27728  pntlem3  27824  elleft  28095  elright  28096  elons  28497  elreno  28735  axcontlem2  29370  lfgredgge2  29529  uspgredg2vlem  29631  uspgredg2v  29632  usgredg2vlem1  29633  usgredg2vlem2  29634  ushgredgedg  29637  ushgredgedgloop  29639  uhgrspan1  29711  upgrreslem  29712  umgrreslem  29713  isfusgr  29726  nbupgrres  29772  nbusgredgeu0  29776  nbusgrf1o0  29777  uvtxel  29796  uvtxel1  29804  cusgrexilem2  29850  cusgrfilem2  29864  vtxdginducedm1lem4  29950  rgrx0ndm  30001  iswspthn  30265  wwlknon  30273  wspthnon  30274  wwlksn0  30279  wwlksnextfun  30314  wwlksnextinj  30315  wwlksnextsurj  30316  wwlksnextproplem3  30327  clwlkclwwlkflem  30422  clwlkclwwlkfolem  30425  isclwwlkn  30445  clwwlkel  30464  clwwlkf  30465  clwwlkf1  30467  isclwwlknon  30509  s2elclwwlknon2  30522  isfrgr  30682  frgrwopreglem3  30736  frgrwopreglem5lem  30742  frgrwopreglem5  30743  isablo  30969  iscbn  31287  hcau  31607  issh  31631  isch  31645  elcnop  32280  ellnop  32281  elbdop  32283  elhmop  32296  elcnfn  32305  ellnfn  32306  isst  32636  ishst  32637  ela  32762  isslmd  33586  elrgspnlem1  33626  elrgspnlem2  33627  elrgspnlem4  33629  elrgspn  33630  ssmxidllem  33820  isufd  33894  iscref  34298  isrrext  34454  ispisys  34607  isldsys  34611  isros  34623  issros  34630  oddpwdc  34809  eulerpartleme  34818  eulerpartlemo  34820  eulerpartlemd  34821  eulerpartlemt0  34824  eulerpartlemf  34825  eulerpartlemt  34826  eulerpartlemr  34829  eulerpartlemmf  34830  eulerpartlemgvv  34831  eulerpartlemgs2  34835  eulerpartlemn  34836  elprob  34864  ballotlemelo  34943  ballotleme  34952  bnj1152  35451  bnj1280  35473  elscott  35568  elscott2  35571  elscottrank  35572  subfacp1lem3  35711  subfacp1lem5  35713  erdszelem1  35720  ispconn  35752  issconn  35755  cvmsiota  35806  cvmlift2lem12  35843  fmla1  35916  gonan0  35921  goaln0  35922  gonar  35924  goalr  35926  sategoelfvb  35948  rdgprc0  36320  elwlim  36350  neibastop1  36927  neibastop2lem  36928  neibastop2  36929  topdifinffinlem  38050  pibp19  38117  pibp21  38118  poimirlem5  38333  poimirlem6  38334  poimirlem7  38335  poimirlem8  38336  poimirlem10  38338  poimirlem11  38339  poimirlem12  38340  poimirlem15  38343  poimirlem16  38344  poimirlem17  38345  poimirlem18  38346  poimirlem19  38347  poimirlem20  38348  poimirlem21  38349  poimirlem22  38350  isprrngo  38759  rabeqel  38964  toycom  39805  isopos  40012  isoml  40070  isatl  40131  iscvlat  40155  ishlat1  40184  cdlemm10N  41950  dihglblem2N  42126  lcfl1lem  42323  lcfls1lem  42366  mapdordlem1a  42466  mapdordlem1  42468  iscsrg  42796  readvcot  43183  mhphflem  43386  pellqrex  43664  islnm  43862  pwssplit4  43874  islnr  43896  fnlimcnv  46439  stoweidlem14  46786  stoweidlem16  46788  stoweidlem37  46809  stoweidlem48  46820  stoweidlem51  46823  stoweidlem59  46831  salexct  47106  salexct2  47111  salexct3  47114  salgencntex  47115  salgensscntex  47116  ovn0lem  47337  opnvonmbllem1  47404  ovolval5lem2  47425  pimincfltioc  47488  pimdecfgtioo  47489  pimincfltioo  47490  smfresal  47560  smfmullem2  47564  smfpimbor1lem1  47570  smfpimbor1lem2  47571  smfinflem  47589  sprsymrelfo  48304  prproropf1olem1  48310  pairreueq  48317  iseven  48451  isodd  48452  m1expevenALTV  48470  iseven2  48474  isodd3  48475  odd2np1ALTV  48497  opoeALTV  48506  opeoALTV  48507  isgbe  48574  isgbow  48575  isgbo  48576  uspgrlimlem2  48812  uspgrlimlem3  48813  uspgrlimlem4  48814  clnbgrvtxedg  48817  grlimpredg  48821  grlimprclnbgrvtx  48822  grlimgrtrilem1  48824  0nodd  48992  1odd  48993  2nodd  48994  iscmgmALT  49046  issgrpALT  49047  iscsgrpALT  49048  1neven  49060  2zlidl  49062  2zrngamgm  49067  2zrngagrp  49071  2zrngmmgm  49074  2zrngnmrid  49078  isprmrng  49158  itsclc0  49608  itsclc0b  49609  isthinc  50254  istermc  50309