Theorem oprex 3018

Description: The result of an operation is a set.

Assertion

Ref	Expression
oprex	⊢ (AFB) ∈ V

Proof of Theorem oprex

Step	Hyp	Ref	Expression
1		df-opr 3003	. 2 ⊢ (AFB) = (F ‘⟨A, B⟩)
2		fvex 2838	. 2 ⊢ (F ‘⟨A, B⟩) ∈ V
3	1, 2	eqeltr 1159	1 ⊢ (AFB) ∈ V

Syntax hints:   ∈ wcel 1092  Vcvv 1348  ⟨cop 1810   ‘cfv 2422  (class class class)co 3001

This theorem is referenced by:  ndmoprass 3062  ndmoprdistr 3063  ndmord 3064  ndmordi 3065  caopr4 3078  caopr411 3079  caoprdistrr 3081  caoprdilem 3082  caoprlem2 3083  oasuc 3131  omsuc 3133  oesuc 3134  oacl 3138  omcl 3139  oecl 3140  oaordi 3148  oaass 3163  brecop2 3243  ecopoprtrn 3247  th3qlem1 3250  mapsnen 3334  map1 3335  mapen 3386  mapdom1 3387  mapdom2 3389  mapxpen 3390  xpmapenlem5 3395  mapunen 3397  pwen 3398  unfilem2 3439  unfilem3 3440  aleph1 3676  cdainf 3731  addcmpblnq 3846  ordpipq 3850  addcompq 3856  addasspq 3857  distrpq 3861  recmulpq 3864  ltsopq 3869  ltapq 3870  ltmpq 3871  1lt2pq 3872  ltaddpq 3873  ltexpq 3874  halfpq 3876  ltbtwnpq 3878  ltrpq 3879  genpprecl 3898  genpn0 3900  genpnnp 3902  genpnmax 3904  genpass 3906  1pr 3911  addclprlem1 3912  addclprlem2 3913  mulclprlem 3915  distrlem1pr 3921  distrlem4pr 3924  distrlem5pr 3925  1idpr 3927  prlem934a 3931  prlem934b 3932  prlem934 3933  ltexprlem4 3939  ltexprlem7 3942  ltapr 3945  prlem936a 3947  prlem936 3949  reclem3pr 3952  reclem4pr 3953  mulcmpblnrlem 3976  mulcmpblnr 3977  ltsrpr 3980  mulcomsr 3992  distrsr 3994  m1m1sr 3996  ltsosr 3997  0lt1sr 3998  1idsr 4001  ltasr 4003  pn0sr 4004  negexsr 4005  recexsrlem 4006  addgt0sr 4007  mulgt0sr 4008  sqgt0sr 4009  recexsr 4010  ssgt0sr 4011  mappsrpr 4012  ltpsrpr 4013  map2psrpr 4014  supsrlem1 4019  supsrlem2 4020  supsrlem3 4021  supsrlem6 4024  axmulcom 4071  axmulass 4073  axdistr 4074  axrecex 4079  axrnegex 4080  axrrecex 4081  axi2m1 4082  axltadd 4085  axmulgt0 4086  peano2nn 4433  nnind 4434  nn1suc 4435  sup2 4510  nnunb 4520  uzind 4603  elq 4629  om2uzsuc 4652  seqlem1 4662  seqsuclem 4669  cjvalt 4799  facp1t 4873  ruclem8 4892  ruclem13 4897  ruclem16 4900  ruclem18 4902  ruclem19 4903  ruclem20 4904  ruclem21 4905  ruclem25 4909  qnnen 4931  infmap1 4950  infmap2lem2 4952  infmap2 4953  alephexp2 4956  hvsubvalt 4997  hsn0elch 5155  occllem3 5182  occllem6 5185  occllem7 5186  shintcl 5294  hosmvalt 5487  hodmvalt 5488  hosvalt 5489  hodvalt 5490  strlem2 5692

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-uni 1920  df-fv 2438  df-opr 3003

metamath.org