Theorem elrab 3331

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 3329	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:  elrab3  3332  elrab2  3333  ralrab  3335  rexrab  3337  rabsnt  4210  unimax  4409  ssintub  4430  intminss  4438  rabxfrd  4815  ssimaex  6173  weniso  6504  canth  6508  sorpsscmpl  6846  onnminsb  6896  dfom2  6959  ssnlim  6975  elsuppfn  7190  ressuppssdif  7203  oeeulem  7568  nnawordex  7604  elpmg  7759  fineqvlem  8059  mapfienlem2  8194  supub  8248  suplub  8249  ordtypelem6  8311  ordtypelem7  8312  hartogslem1  8330  hartogs  8332  wemapsolem  8338  card2on  8342  elharval  8351  wdom2d  8368  cantnfs  8446  oemapvali  8464  rankuni2b  8599  scottex  8631  tskwe  8659  cardid2  8662  iscard2  8685  harval2  8706  cardmin2  8707  acni3  8753  alephsuc2  8786  kmlem1  8855  cofsmo  8974  coftr  8978  fin23lem11  9022  enfin2i  9026  fin1a2lem9  9113  fin1a2lem11  9115  axcc4  9144  axdc3lem2  9156  zorn2lem7  9207  ondomon  9264  alephval2  9273  grutsk  9523  pinq  9628  negf1o  10339  fiminre  10851  infm3  10861  nnind  10915  peano2uz2  11341  peano5uzi  11342  dfuzi  11344  uzind  11345  uzind3  11347  eluz1  11567  uzind4  11622  nnwos  11631  eqreznegel  11650  zsupss  11653  zmin  11660  elixx1  12055  elioo2  12087  elfz1  12202  flval3  12478  serge0  12717  expge0  12758  expge1  12759  hashbclem  13093  pr2pwpr  13116  elss2prb  13123  hash2sspr  13124  elss2prOLD  13125  wrdmap  13191  wwlktovfo  13549  shftf  13667  rlimrege0  14158  incexc2  14409  dvdsdivcl  14876  divalglem4  14957  divalgmod  14967  divalgmodOLD  14968  bitsval  14984  bezout  15098  dfgcd2  15101  lcmledvds  15150  lcmgcdlem  15157  lcmfledvds  15183  1nprm  15230  1idssfct  15231  isprm2  15233  phicl2  15311  hashdvds  15318  phisum  15333  odzval  15334  odzcllem  15335  odzdvds  15338  pcpremul  15386  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  ramub  15555  rami  15557  ramub1lem1  15568  ramub1lem2  15569  prmgaplem3  15595  prmgaplem4  15596  prmgaplem5  15597  prmgaplem6  15598  ismre  16073  mrcflem  16089  mrcval  16093  ismri  16114  isacs  16135  isacs1i  16141  catlid  16167  catrid  16168  ismon  16216  isnat  16430  eldmcoa  16538  coaval  16541  fncnvimaeqv  16583  lubeldm  16804  glbeldm  16817  gsumress  17099  gsumval2  17103  ismhm  17160  issubm  17170  issubmd  17172  mhmeql  17187  mrcmndind  17189  grplinv  17291  issubg  17417  cycsubg  17445  isnsg  17446  ghmeql  17506  isgim  17527  isga  17547  elcntz  17578  elcntzsn  17581  symgfix2  17659  pmtrval  17694  pmtrrn  17700  symgsssg  17710  symgfisg  17711  psgnunilem5  17737  odid  17780  odlem2  17781  gexid  17819  gexlem2  17820  gexdvds  17822  isslw  17846  pgpssslw  17852  pj1id  17935  efgsfo  17975  oddvdssubg  18081  dprdwd  18233  pgpfac1lem5  18301  ablfaclem2  18308  isirred  18522  isrim0  18546  issubrg  18603  isabv  18642  islss  18756  islmhm  18848  lmhmeql  18876  islmim  18883  islbs  18897  gsumbagdiaglem  19196  psrmulcllem  19208  psrlidm  19224  psrridm  19225  psrass1  19226  psrcom  19230  mplsubglem  19255  mpllsslem  19256  mplmonmul  19285  evlsval2  19341  coe1fsupp  19405  coe1ae0  19407  coe1mul2  19460  zrhcofipsgn  19758  psgndiflemB  19765  elocv  19831  isobs  19883  dsmmelbas  19902  frlmelbas  19919  frlmssuvc2  19953  islinds  19967  dmatel  20118  dmatmulcl  20125  scmatel  20130  scmateALT  20137  symgmatr01lem  20278  pmatcoe1fsupp  20325  cpmatel  20335  chpscmat  20466  istopon  20540  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  epttop  20623  iscld  20641  clscld  20661  isnei  20717  neips  20727  neiptopnei  20746  iscn  20849  iscnp  20851  ordthauslem  20997  cmpsublem  21012  concompcon  21045  2ndc1stc  21064  2ndcdisj  21069  locfincmp  21139  elkgen  21149  xkoopn  21202  xkoccn  21232  txdis1cn  21248  pthaus  21251  txkgen  21265  xkohaus  21266  xkococnlem  21272  xkococn  21273  xkoinjcn  21300  txcon  21302  elqtop  21310  nrmr0reg  21362  elmptrab  21440  fbssfi  21451  opnfbas  21456  elfg  21485  cfinfil  21507  csdfil  21508  supfil  21509  filssufilg  21525  uffix  21535  fixufil  21536  uffixfr  21537  uffixsn  21539  ufinffr  21543  ufilen  21544  elflim2  21578  supnfcls  21634  fclscf  21639  flimfnfcls  21642  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem2  21667  tmdgsum2  21710  symgtgp  21715  ghmcnp  21728  elutop  21847  isucn  21892  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  elblps  22002  elbl  22003  restmetu  22185  icccmp  22436  elcncf  22500  ishtpy  22579  isphtpy  22588  om1elbas  22640  iscfil  22871  iscau  22882  iscmet  22890  lmle  22907  rrxfsupp  22993  minveclem3  23008  minveclem4  23011  ovolshftlem1  23084  ovolscalem1  23088  ovolicc2lem3  23094  iundisj  23123  dyadmax  23172  dyadmbllem  23173  opnmbllem  23175  vitalilem2  23184  vitalilem3  23185  elcpn  23503  ig1pval3  23738  coelem  23786  quotlem  23859  elqaalem1  23878  elqaalem3  23880  aannenlem1  23887  aannenlem2  23888  aalioulem2  23892  radcnv0  23974  dmarea  24484  jensen  24515  ftalem4  24602  ftalem5  24603  efnnfsumcl  24629  efchtdvds  24685  sqff1o  24708  fsumdvdsdiaglem  24709  dvdsppwf1o  24712  dvdsflf1o  24713  dvdsflsumcom  24714  musum  24717  muinv  24719  logfac2  24742  dchrelbas  24761  dchrfi  24780  lgsfle1  24831  lgsle1  24837  lgsdirprm  24856  lgsne0  24860  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1b  24917  dchrvmasumlem1  24984  logsqvma  25031  pntleml  25100  tgellng  25248  mircgr  25352  mirbtwn  25353  iseqlg  25547  ttgelitv  25563  upgrle  25757  upgrbi  25760  umgredg2  25766  umgrbi  25767  upgr1elem  25778  edgupgr  25808  edgumgr  25809  upgredg  25811  umgrale  25850  umgra1  25855  edg  25882  uslgra1  25901  usgra1  25902  usgraedg2  25904  usgraedgrnv  25906  usgrarnedg  25913  usgraedg4  25916  usgraexmplef  25929  usgrares1  25939  nbgrael  25955  nbgraeledg  25959  nbgraf1olem3  25972  cusgrarn  25988  nbcusgra  25992  cusgrares  26001  uvtxel  26017  uvtxnbgra  26021  cusgrauvtxb  26024  iswwlk  26211  iswwlkn  26212  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextsur  26259  wlknwwlknvbij  26268  isclwwlk  26296  isclwwlkn  26297  clwwlkprop  26298  clwwlknprop  26300  clwwlkvbij  26329  clwwlknscsh  26347  eleclclwwlkn  26360  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  el2wlksoton  26405  el2spthsoton  26406  el2wlksotot  26409  rusgranumwlklem0  26475  rusgranumwlklem1  26476  rusgranumwlklem3  26478  rusgranumwlks  26483  eupath2  26507  umgrabi  26510  konigsberg  26514  2spotdisj  26588  usg2spot2nb  26592  usgreg2spot  26594  numclwwlkun  26606  numclwwlkovfel2  26610  numclwwlkovgel  26615  numclwlk1lem2foa  26618  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  grpoidinv2  26753  grpoinv  26763  isssp  26963  islno  26992  isblo  27021  ishmo  27050  ubthlem1  27110  ubthlem2  27111  htthlem  27158  ocel  27524  shsval2i  27630  ococin  27651  chsupsn  27656  eleigvec  28200  cnlnadjlem5  28314  shatomistici  28604  hatomistici  28605  nnindf  28952  ordtconlem1  29298  indf1ofs  29415  sigagenval  29530  ldsysgenld  29550  ldgenpisyslem1  29553  ldgenpisyslem2  29554  ldgenpisys  29556  ddemeas  29626  ismbfm  29641  imambfm  29651  dya2iocuni  29672  oms0  29686  omssubadd  29689  elcarsg  29694  issibf  29722  sitgfval  29730  oddpwdc  29743  eulerpartlemgh  29767  eulerpartlemgs2  29769  dstfrvel  29862  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemiex  29890  ballotlemfrcn0  29918  ballotlemirc  29920  ballotlem7  29924  conpcon  30471  iscvm  30495  cvmsi  30501  cvmsval  30502  cvmliftmolem2  30518  cvmliftiota  30537  snmlval  30567  elmpst  30687  sltval2  31053  sltres  31061  nodenselem7  31086  nofulllem5  31105  lineelsb2  31425  linerflx1  31426  fwddifval  31439  fwddifnval  31440  rankeq1o  31448  finminlem  31482  fneint  31513  fnessref  31522  topmeet  31529  topjoin  31530  neifg  31536  relowlssretop  32387  fin2solem  32565  fin2so  32566  poimirlem4  32583  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  opnmbllem0  32615  mblfinlem2  32617  itg2gt0cn  32635  indexa  32698  nninfnub  32717  istotbnd  32738  sstotbnd2  32743  isbnd  32749  isrngohom  32934  isrngoiso  32947  isidl  32983  ispridl  33003  ismaxidl  33009  prnc  33036  isfldidl  33037  islshp  33284  lssats  33317  islfl  33365  isat  33591  atlatmstc  33624  islln  33810  islpln  33834  islvol  33877  linepsubN  34056  elpmap  34062  pmapsub  34072  elpadd  34103  paddvaln0N  34105  islhp  34300  isldil  34414  isltrn  34423  isdilN  34459  istrnN  34462  diaval  35339  diaelval  35340  diaeldm  35343  diaelrnN  35352  cdlemm10N  35425  docaclN  35431  dibglbN  35473  dicval  35483  dicfnN  35490  dicvalrelN  35492  dihglblem2aN  35600  dihglblem2N  35601  dihglblem3N  35602  dih1dimatlem  35636  dihglb2  35649  dochvalr  35664  doch2val2  35671  dochocss  35673  islpolN  35790  mapd0  35972  isnacs  36285  elmzpcl  36307  mzpindd  36327  rencldnfilem  36402  irrapxlem6  36409  pellexlem3  36413  pellexlem5  36415  elpell1qr  36429  elpell14qr  36431  elpell1234qr  36433  pellfundre  36463  pellfundge  36464  pellfundlb  36466  pellfundglb  36467  rmspecnonsq  36490  jm2.22  36580  jm2.23  36581  rpnnen3lem  36616  fnwe2lem2  36639  fnwe2lem3  36640  elmnc  36725  dgraalem  36734  dgraaub  36737  mpaalem  36741  rgspnmin  36760  issdrg  36786  rfovcnvf1od  37318  nzss  37538  iccshift  38591  iooshift  38595  limcperiod  38695  sumnnodd  38697  ioodvbdlimc1lem1  38821  dvnprodlem1  38836  dvnprodlem3  38838  itgperiod  38873  stoweidlem14  38907  stoweidlem15  38908  stoweidlem16  38909  stoweidlem31  38924  stoweidlem36  38929  stoweidlem46  38939  stoweidlem48  38941  fourierdlem2  39002  fourierdlem3  39003  fourierdlem20  39020  fourierdlem25  39025  fourierdlem37  39037  fourierdlem42  39042  fourierdlem48  39047  fourierdlem51  39050  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem79  39078  fourierdlem81  39080  elaa2lem  39126  etransclem24  39151  etransclem26  39153  etransclem28  39155  etransclem35  39162  etransclem48  39175  salgenval  39217  salgenn0  39225  salgencl  39226  sssalgen  39229  salgenss  39230  salgenuni  39231  issalgend  39232  salgencntex  39237  subsaliuncllem  39251  sge0fodjrnlem  39309  meadjiunlem  39358  caragenel  39385  ovnlecvr  39448  ovnpnfelsup  39449  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  ovnhoilem1  39491  ovnlecvr2  39500  ovncvr2  39501  issmflem  39613  smflimlem2  39658  smflimlem3  39659  iccpart  39954  iseven  40079  isodd  40080  dfodd2  40087  dfeven5  40116  dfodd7  40117  edgusgr  40391  usgruspgrb  40411  usgredg2ALT  40420  ushgredgedga  40456  ushgredgedgaloop  40458  subumgredg2  40509  subupgr  40511  upgrres1  40532  nbgrel  40564  nbupgrel  40567  nbumgrvtx  40568  nbusgreledg  40575  nbgrnself  40583  nbusgredgeu0  40596  nbusgrf1o0  40597  uvtxael  40614  uvtxael1  40622  uvtxusgrel  40630  1hevtxdg1  40721  1hegrlfgr  40722  umgr2v2e  40741  rgrusgrprc  40789  rgrx0ndm  40793  lfgrwlkprop  40896  iswwlks  41039  iswwlksn  41041  wwlknon  41053  wspthnon  41054  wwlksn0  41059  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnextsur  41106  wlksnwwlknvbij  41114  wwlks2onv  41158  rusgrnumwwlks  41177  isclwwlks  41188  isclwwlksn  41190  clwwlksvbij  41229  clwwlksnscsh  41247  eleclclwwlksn  41260  clwwlksnun  41281  eupth2lems  41406  konigsberglem4  41425  fusgr2wsp2nb  41498  fusgreg2wsp  41500  2wspmdisj  41501  av-numclwwlkovfel2  41514  av-numclwwlkovgel  41519  av-numclwlk1lem2foa  41521  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  ismgmhm  41573  issubmgm  41579  rabsubmgmd  41581  mgmhmeql  41593  assintop  41635  isassintop  41636  assintopcllaw  41638  isrnghm  41682  isrngisom  41686  0even  41721  2even  41723  2zrngamgm  41729  dmatALTbasel  41985  lcoval  41995  elbigo  42143  secval  42287  cscval  42288  cotval  42289