Theorem fveq2 4681

Description: Equality theorem for function value.

Assertion

Ref	Expression
fveq2	|- (A = B -> (F` A) = (F` B))

Proof of Theorem fveq2

Step	Hyp	Ref	Expression
1		sneq 3054	. . . . . 6 |- (A = B -> {A} = {B})
2	1	imaeq2d 4264	. . . . 5 |- (A = B -> (F"{A}) = (F"{B}))
3	2	eqeq1d 1892	. . . 4 |- (A = B -> ((F"{A}) = {x} <-> (F"{B}) = {x}))
4	3	abbidv 2008	. . 3 |- (A = B -> {x | (F"{A}) = {x}} = {x | (F"{B}) = {x}})
5	4	unieqd 3188	. 2 |- (A = B -> U.{x | (F"{A}) = {x}} = U.{x | (F"{B}) = {x}})
6		df-fv 4014	. 2 |- (F` A) = U.{x | (F"{A}) = {x}}
7		df-fv 4014	. 2 |- (F` B) = U.{x | (F"{B}) = {x}}
8	5, 6, 7	3eqtr4g 1953	1 |- (A = B -> (F` A) = (F` B))

Syntax hints:   -> wi 3   = wceq 1298  {cab 1871  {csn 3044  U.cuni 3177  "cima 3989  ` cfv 3998

This theorem is referenced by:  fveq2i 4684  fveq2d 4685  tz6.12-2 4696  funbrfv 4709  fnbrfvb 4712  dffn5 4717  ssimaex 4729  eqfnfv2f 4770  elrnopabg 4773  fvelrn 4785  ffnfvf 4802  fnressn 4812  fressnfv 4813  fopabsnOLD 4816  fvi 4818  fconstfv 4825  fvresex 4833  abrexexlem2 4835  funiunfv 4842  funiunfvf 4846  dff13f 4851  f1fveq 4852  f1ocnvfv 4856  f1ocnvfvb 4857  f1ocnvfv3 4859  isorel 4871  isocnv 4873  isotr 4874  isotrALT 4875  f1owe 4882  f1oweALT 4883  ffnoprv 4943  eqfnoprv 4945  fnoprv 4946  fnrnoprv 4966  fooprv 4967  oprvexOLDOLD 4974  1stval2 5030  2ndval2 5031  1st2val 5038  2nd2val 5039  eqop 5044  unielxp 5047  sbcopeq1a 5051  csbopeq1a 5052  dfopab2 5053  dfoprab3 5054  dfoprab5s 5057  elrnoprabg 5066  df1st2 5068  df2nd2 5069  1stconst 5070  2ndconst 5071  fsplit 5086  canth 5112  onfununi 5116  tfrlem1 5119  tfrlem2 5120  tfrlem11 5129  tfr2 5133  tfr3 5134  tz7.44-1 5136  tz7.44-2 5137  tz7.44-3 5138  rdglem1 5145  rdglem2 5146  rdgsuc 5153  rdglim 5156  tz7.48lem 5164  tz7.49 5168  abianfplem 5170  abianfp 5171  oav 5195  omv 5196  oev 5198  oev2 5207  omsmolem 5313  dom2d 5463  ac6sfilem3 5508  mapenlem2 5584  unblem2 5634  ordiso 5683  ordtypelem5 5688  ordtypelem7 5690  hartoglem 5692  inf3lemd 5718  inf3lem1 5719  inf3lem2 5720  inf3lem5 5723  trcl 5752  r1tr 5765  r1ord 5766  r1ord3 5768  r1val1 5769  tz9.12lem3 5772  tz9.12 5773  rankvalg 5780  rankr1 5785  rankr1g 5786  ranklim 5796  r1pwcl 5798  ranksn 5800  rankonid 5806  rankeq0 5807  rankr1id 5808  rankuni 5809  rankxplim 5823  scottex 5846  scott0 5847  scottexs 5848  scott0s 5849  karden 5856  alephon 5876  omsubsdomlem2 5880  omsubsdom 5881  omsubdom 5882  omsubel 5883  elomsubsd 5885  omsublim 5887  omsubindss 5888  infenomsub 5889  omsubinit 5890  aceq3lem 5894  aceq4 5896  aceq5 5902  aceq6b 5904  ac6lem 5916  numthlem 5945  numth 5946  zorn2lem6 5955  unidom 5970  uniimadomf 5973  oncard 5978  carduni 6010  cardiun 6011  cardprc 6013  alephcard 6015  alephordlem2 6021  alephordi 6022  alephord 6023  alephle 6032  cardaleph 6033  cardalephex 6034  alephfplem2 6045  alephfplem3 6046  alephfplem4 6047  alephfp2 6049  alephval2 6050  alephval3 6051  cf0 6058  cardcf 6059  cflecard 6060  cfeq0 6062  cfsuc 6063  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  monoord 7523  icoshftf1oii 7578  uz11 7601  fzprval 7687  fztpval 7688  fsequb 7702  om2uzsuci 7707  om2uzuzi 7708  om2uzlti 7709  om2uzlt2i 7710  cardfz 7719  seq1lem1 7722  seq1rval 7724  seq1val2 7727  seq1suclem 7729  seq1rn2 7734  seq1res 7740  ser1recli 7744  ser1monoi 7750  ser1add2i 7751  ser1addi 7752  seq1shftid 7769  seqzfval 7780  seqzfveq 7797  seqzrn2 7799  seqzres2 7804  ser0cl1i 7807  expval 7813  sqrthi 7949  sqrcli 7950  sqrgt0i 7951  sqrge0i 7952  sqr11i 7953  sqrmuli 7955  sqrcl 7960  sqrgt0 7961  sqrge0 7962  sqrle 7963  sqr00 7964  sqsqr 7973  absval 8012  cjval 8013  cjreb 8050  cjmulrcl 8051  cjmulval 8052  cjmulge0 8053  reneg 8054  readd 8055  imneg 8057  imadd 8058  cjcj 8061  cjadd 8062  cjmul 8063  cjneg 8064  addcj 8065  cj11 8080  abs00i 8093  absval2 8103  abs00 8104  absge0 8105  absmul 8109  absdiv 8111  absid 8113  abslt 8132  absle 8133  abssubne0 8134  cjdiv 8141  absgt0 8145  abstri 8150  abs1mi 8156  abslem2 8161  seq1bndi 8162  seq1ublem 8163  cau2i 8165  caurei 8179  cauimi 8180  ser1absdiflem 8181  facp1 8188  faccl 8192  facdiv 8194  facwordi 8196  faclbnd 8197  faclbnd4lem1 8200  faclbnd4lem2 8201  faclbnd4lem3 8202  faclbnd4lem4 8203  bcval 8210  hashen 8233  dffsum 8258  fsumserzfi 8260  ser1ser0i 8308  serzcl2 8309  serz1p 8312  serzmulci 8318  serzrelem 8321  clm4a 8350  clmi2a 8351  climconst3 8356  climshfti 8364  iserzshft2i 8367  serzclim0 8369  climrecl 8370  climge0 8372  climaddlem1 8374  climaddlem3 8376  climmullem6 8385  climmullem8 8387  climsub 8390  climcmplem 8397  climabslem 8408  climubii 8413  climubi 8414  climcaui 8416  caucvglem2 8418  caucvgi 8423  caucvg3i 8427  caucvg3 8428  serzf0i 8429  ser1consti 8431  ser1cmpi 8434  ser1cmp2i 8437  iserzabsi 8439  cvgcmp2lem 8440  cvgcmp2i 8441  cvgcmp2ci 8444  cvgcmp3cei 8448  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  isumvaltfi 8454  isum1p 8467  isumnn0nnai 8469  iserzgt0 8472  isummulc1 8473  isummulc1iALT 8474  isummulc1ai 8475  isumcmpii 8476  reccnv 8479  expcnv 8494  explecnv 8495  geoseri 8496  geolimi 8498  geolim 8499  geolim1 8501  geoisumr 8505  cvgratlem1ALT 8509  cvgratlem3ALT 8511  cvgratlem1 8512  cvgratlem3 8514  cvgratlem4 8515  negfcncfi 8531  ivthlem4 8546  ivthlem6 8548  ivthlem7 8549  ivthlem8 8550  ivthlem9 8551  dsupivthlem 8553  efcltlem1 8566  dfef2i 8569  ef0lem 8572  efcl 8574  efcvg 8576  eftval 8578  reefcl 8580  erelem3 8583  erelem6 8586  ege2lem2 8590  ege2le3lem2 8591  efcj 8599  efaddlem6 8605  efadd 8629  ef1tlubi 8644  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  ef01tlubi 8648  absef01tlubi 8650  ef4p 8665  efgt0i 8669  efgt0 8670  efltbi 8672  reef11 8674  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  reeff1olem1 8689  reeff1o 8691  reefiso 8693  sinadd 8718  cosadd 8719  absef 8749  efieq1re 8751  acdc3lem 8754  acdc3 8755  acdclem 8763  acdc 8764  acdcALT 8765  ruclem4 8782  ruclem25 8803  ruclem29 8807  ruclem33 8811  ruclem35 8813  ruclem37 8815  infmap2lem2 8849  clsfval 8944  0ntr 8978  lpfval 9018  cnpval 9035  metxpdval 9106  metxp 9111  opnfval 9134  methaus 9160  metcni 9172  iscau3 9216  iscau4 9218  iscaunns 9222  iscms 9224  lmfexlem2 9235  lmle 9238  metelcls 9243  metcnp4lem1 9246  metcnp4lem2 9247  metcnp4 9248  metcn4i 9250  xplmi 9251  xplm 9253  xpcn 9254  bopcnlem2 9260  fsumcnlem 9267  lmcau 9274  bcthlem2 9278  bcthlem10 9286  bcthlem15 9291  bcthlem16 9292  bcthlem17 9293  bcthlem18 9294  bcthlem20 9296  bcthlem28 9304  bcthlem29 9305  bcthlem33 9309  bcth 9310  grpidval 9342  grpinvfval 9350  grpinvf 9364  grpdivfval 9366  grpdivval 9367  gxoprval 9380  gxval 9381  gxcom 9392  gxid 9396  ghgrpilem1 9441  isgalem 9449  nvvcop 9545  bafval 9555  isnvlem 9561  nvi 9565  nvs 9622  nvz 9629  nvtri 9630  imsval 9648  imsmet 9656  vacnlem1 9667  vacnlem3 9669  vacnlem4 9670  vacnlem5 9671  vacnlem6 9672  vacn 9673  sqcn 9674  nmcn 9678  ipfval 9691  iporthcom 9708  ip1cnilem2 9713  sspval 9721  isssp 9722  lnoval 9752  lnolin 9754  nmofval 9764  nmosetn0 9767  nmolb 9773  nmoubi 9774  nmounbseqi 9779  nmobndseqi 9780  isblo 9782  0ofval 9787  nmo0 9791  nmlno0lem 9793  nmlno0i 9794  nmlnoubi 9796  lnon0 9798  nmblolbii 9799  nmblolbi 9800  blocnilem 9804  ajfval 9809  ishmo 9811  phpar2 9823  phpar 9824  ipdir 9843  ipass 9846  sii 9855  isbn 9866  ubthlem1 9872  ubthlem3 9874  minveclem6 9895  minveclem7 9896  minveclem8 9897  minveclem23 9912  minveclem27 9916  minveclem33 9922  minveceu 9928  htthlem2 9968  htthlem3 9969  htthlem4 9970  sincolem 10014  pilem1 10020  pilem2 10021  pilem3 10022  pilem4 10023  sineq0re 10067  cosh111lem2 10069  cosh111 10071  efif 10075  efifolem1 10076  efifolem2 10077  efifolem3 10078  efifolem6 10081  efifo 10083  efif1lem5 10088  efielcirc 10093  circgrp 10094  eff1i 10098  effoi 10099  pilog 10122  logltb 10130  xp1st 10155  xp2nd 10156  oprabopabf 10157  oprabco 10159  findcardOLD 10179  ghomlin 10196  fibas 10221  upxp 10225  uptx 10226  txcnopab 10228  2txcn 10229  fsubbas 10281  fgf 10283  sfvlim 10296  hausfillim 10303  flimff 10317  sflimf 10318  hausfillim2 10325  ist1 10336  iscon 10339  iscon2 10340  on1el3 10412  on1el4 10413  isdivrng 10417  orthcom 10607  normlem7tALT 10618  normsq 10634  norm-ii 10638  norm-iii 10640  normpyth 10645  normpar 10655  bcsiALT 10679  bcs 10681  hcau2 10688  hlimcauii 10739  norm1exi 10755  occllem3 10808  occllem5 10810  occl 10815  projlem22 10840  projlem23 10841  projlem26 10844  pjthlem8 10859  pjth 10867  pjtheu 10869  pjmval 10871  omlsi 10879  ococ 10881  axpjpj 10889  pjoc1 10900  pjoml 10902  pjoc2 10905  chocin 11051  chsscon3 11056  chjo 11071  chdmm1 11081  spanun 11101  hosval 11149  hosvalOLD 11150  homval 11151  hodval 11152  hodvalOLD 11153  hfsval 11154  hfmval 11155  cmbr 11160  pjoml6i 11165  cmbr3 11184  pjoml2 11187  pjoml3 11188  cmcm3 11191  osumlem8 11220  osum 11223  pjch1 11250  pjadji 11265  pjaddi 11266  pjinormi 11267  pjsubi 11268  pjmuli 11269  pjige0 11271  pjcjt2 11272  pjch 11274  pjjsi 11280  pjrni 11282  pjfo 11286  pj11i 11291  pj11 11294  pjopyth 11300  pjnorm 11304  pjpyth 11305  pjnel 11306  adjsym 11396  eigre 11398  eigorth 11401  elbdop 11424  nmopsetn0 11429  nmfnsetn0 11442  eigvalval 11460  nmoplb 11468  nmopub 11469  cnopc 11474  lnopl 11475  unop 11476  hmop 11483  nmfnlb 11485  nmfnleub 11486  elnlfn 11489  cnfnc 11491  lnfnl 11492  adj1 11494  eleigvec 11518  eigval1 11521  nmop0 11547  nmfn0 11548  nmlnop0iALT 11557  nmlnop0 11560  lnopeq0lem2 11568  lnopeq0i 11569  lnopunilem1 11572  lnopunii 11574  elunop2 11575  lnophmlem1 11578  lnophmi 11580  lnophm 11581  nmbdoplbi 11586  nmbdoplb 11587  nmcopexlem6 11593  nmcoplbi 11595  nmcopex 11596  nmcoplb 11597  nmophmi 11598  lnopconi 11600  nmbdfnlbi 11615  nmbdfnlb 11616  nmcfnexlem6 11622  nmcfnlbi 11624  nmcfnex 11625  nmcfnlb 11626  lnfnconi 11627  nlelchi 11631  riesz3i 11632  riesz1 11635  cnlnadjlem1 11637  cnlnadjlem5 11641  adjbd1o 11655  adjeq0 11661  branmfn 11675  branmfnOLD 11676  rnbra 11678  opsqrlem6 11716  pjbdlni 11720  pjhmop 11721  hmopidmchi 11723  hmopidmpji 11724  pjss2coi 11736  pjssmi 11737  pjssge0i 11738  pjdifnormi 11739  pjidmco 11753  pjhmopidm 11754  elpjrnch 11763  pjin2i 11766  pjclem1 11768  hstel2 11791  stge0 11796  stle1 11797  hst1h 11799  stj 11807  strlem1 11822  strlem2 11823  hstrlem2 11831  stcltr1i 11846  dmdmd 11872  atord 11960  irredi 11966  mdsymi 11983  cdj1i 12005  cdj3lem1 12006  cdj3lem2a 12008  cdj3lem2b 12009  cdj3lem3a 12011  cdj3lem3b 12012  cdj3i 12013  bnj141 12473  bnj148 12481  bnj220 12511  bnj897 12817  bnj1063 12899  bnj1078 12905  bnj1271 13030  bnj1534 13183  bnj1542 13190  bnj218 13250  bnj222 13251  bnj223 13252  bnj549 13275  bnj550 13276  bnj552 13277  bnj589 13297  bnj590 13298  bnj591 13299  bnj594 13300  bnj961 13345  bnj1014 13374  bnj1015 13375  bnj1043 13391  bnj1069 13400  bnj1081 13407  bnj1112 13418  bnj1118 13420  bnj1123 13422  bnj1134 13427  bnj1128 13428  bnj1145 13431  bnj1450 13541  bnj1463 13550  bnj1529 13574  bnj1530 13575  fseq1cl 13619  abs2sqle 13624  abs2sqlt 13625  ghomgrpilem1 13628  ghomgrpilem2 13629  ghomsn 13631  ghomgrplem 13632  ghomf1olem 13637  symggrp 13640  cayleylem2 13642  nn0seqcvgd 13659  divalg 13706  gcdcllem1 13718  gcd0id 13729  alginv 13743  algcvg 13744  algcvga 13747  algfx 13748  eucalgval 13749  eucalginv 13752  eucalglt 13753  mulgcdlem1 13756  trcllem1 13933  xporderlem 13948  frxp 13951  poseq 13954  soseq 13955  wfr3g 13956  wfrlem1 13957  wfrlem14 13970  wfr2 13974  tfr3ALT 13979  frr3g 13980  sltval2 13997  axdenselem3 14021  axdenselem5 14023  axdenselem7 14025  axdense 14027  nocvxmin 14029  axfelem1 14031  axfelem3 14033  axfelem4 14034  axfelem5 14035  axfelem7 14037  axfelem8 14038  axfelem9 14039  axfelem12 14042  fveleq 14252  findreccl 14254  findabrcl 14255  fnoprvpop 14338  surrc2 14390  eloi 14400  onsubcum 14442  injrec 14461  surjsec 14462  surjsec2 14467  bclelnu 14495  ispr1 14496  npincppr 14501  repfuntw 14502  repcpwti 14503  cbcpcp 14504  cbicplem 14508  iserzmulc1b 14528  mxlmnl2 14612  prodeq3 14663  dffprod 14670  fprodserzfi 14672  fincmpzer 14711  expus 14726  fprodneg 14741  fprodsub 14742  vecval1b 14794  vecval3b 14795  svs3 14830  nsn 14874  osneisi 14875  usptoplem 14917  istopx 14918  prtoptop 14919  limfillem2 14939  clsingemp 14961  istopgrp 14971  topgrpi 14972  topgrpsubcn 14982  cntrsetlem 14999  1ded 15085  idosd 15091  cmppfd 15092  domcmpd 15093  codcmpd 15094  cmpasso 15120  cmpida 15121  cmpidb 15122  ishoma 15136  ishomc 15138  ishomd 15139  eqidob 15144  ismona 15158  ismonb 15159  ismonb2 15161  isepia 15168  isepib 15169  isepib2 15171  cinvlem1 15176  cinvlem2 15177  isfuna 15182  idfisf 15189  issubcat 15193  issubcata 15194  issubcatb 15195  idsubfun 15206  tarval2g 15250  tmpts 15257  valtar 15260  tartarmap 15265  fictblem 15370  fictb 15371  ordisoOLD 15374  ordtypelem5OLD 15379  ordtypelem7OLD 15381  hartoglemOLD 15383  omsubsdomlem2OLD 15389  omsubsdomOLD 15390  omsubdomOLD 15391  omsubelOLD 15392  elomsubsdOLD 15394  omsublimOLD 15396  omsubindssOLD 15397  infenomsubOLD 15398  omsubinitOLD 15399  fibasOLD 15400  cldbnd 15410  opnregcld 15415  cldregopn 15416  cncls 15419  cnntr 15420  compsub 15431  hscptsscld 15434  alexsublem1 15437  alexsublem3 15439  alexsub 15441  ivthALT 15454  2ndcsb 15476  2ndcctbss 15478  islocfin 15506  comppfsc 15517  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2lem4 15522  neibastop3 15524  isreg 15548  isnrm 15551  flimcls 15588  cnpfillim 15589  sfcls 15604  filclus 15605  isfclus 15606  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomp 15621  ufcomp 15622  fclusff 15623  sfclusf 15624  filnetlem5 15644  filnet 15645  prfOLD 15680  foco2 15686  cocanfo 15689  f1opr 15714  f1elima 15719  cbvixp 15723  upixp 15729  eluzadd 15782  eluzsub 15783  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  seq1eq2 15817  fsumltisum 15824  fsumleisumi 15826  fsumleisum 15827  isumclf 15828  iserzshft2 15829  isumshft2 15830  metf1o 15843  mettrifi 15847  mettrifi2 15848  geomcau 15849  lmclim2 15850  caushft 15851  tlmval 15903  haustlmu 15906  tlmconst 15907  txcnoprab 15911  cnresoprab 15915  cnopropabco 15917  cnoprab1 15921  cnoprab2 15922  txmet 15925  istotbnd 15933  isbnd 15939  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem2 15956  heiborlem3 15957  heiborlem10 15964  heiborlem13 15967  heiborlem16 15970  heiborlem18 15972  heiborlem24 15978  heiborlem25 15979  heiborlem26 15980  heiborlem29 15983  heiborlem30 15984  heiborlem31 15985  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem36 15990  heiborlem42 15996  bfplem3 16000  bfplem5 16002  bfplem6 16003  bfplem8 16005  bfplem9 16006  bfplem10 16007  bfplem11 16008  rrnmet 16016  rrndstprj1 16017  rrndstprj2 16018  rrncms 16019  rrntotbndlem2 16021  ismrer1 16024  ghomco 16040  phtpyid 16049  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  phtpcval 16058  reparphtlem1 16063  reparphtlem2 16064  pcohtpylem3 16082  pcohtpy 16083  pi1bval 16088  pi1fval 16092  rnghomval 16118  rnghomadd 16123  rnghommul 16124  rngisoval 16131  idlval 16161  pridlval 16181  maxidlval 16187  isprrng 16198  igenval 16209  smoel 16451  smoge 16454  addrfv 16469  subrfv 16470  mulvfv 16471  stbval 16731  strcval 16732  stb2xpl 16742  stb3xpl 16743  isposNEW 16773  pltval 16781  pgeval 16794  lubfval 16803  glbfval 16808  joinfval 16814  meetfval 16821  p0val 16843  p1val 16844  islat 16849  isclat 16888  clatlem 16889  clatlat 16893  isopos 16909  oposlem 16913  opcon3b 16923  riotaoc 16936  cmtfval 16937  cmtval 16938  isoml 16959  omllaw 16964  cvrfval 16987  patoms 17000  isatlat 17012  ishlat 17018  glbcon 17028  isgrpNEW 17104  grpidvalNEW 17117  grpinvfvalNEW 17125  isablNEW 17135  isringNEW 17142  ringidval 17149  isdivrngNEW 17160  invrfval 17170  issrng 17176  islvec 17188  isphil 17195  plusssfval 17204  ocvfval 17206  csubspset 17208  iscsubsp 17209  ishil 17210  lineset 17219  pointset 17222  psubspset 17225  pmapfval 17236  pmapglb2 17253  pmapmeet 17255  paddfval 17258  pmapjat 17314  polfval 17317  polat 17341  psubclset 17346  ispsubcl 17347  ispsubcl2 17356  pexmidOLD 17386  watomfval 17392  pautset 17395  dilfset 17401  dilset 17402  trnfset 17404  trnset 17405

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014

Copyright terms: Public domain